-
Notifications
You must be signed in to change notification settings - Fork 1
/
lean_new
executable file
·178 lines (145 loc) · 4.51 KB
/
lean_new
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
#!/bin/sh
#
# shellcheck disable=SC2086 # deliberate splitting
# shellcheck disable=SC2059 # deliberate format variable
# shellcheck disable=SC2142 # deliberate function in alias
# shellcheck disable=SC2317 # code is reachable; shellcheck is wrong
#
# Usage: lean_new PROJECT
# Creates new Lean 4 project named PROJECT in current directory
# with mathlib dependency and an executable default target.
#
# It tries to ensure that lake and elan have the expected behavior
# in order for the project to build and informs the user of any known
# pitfalls.
## Preliminaries
set -u
unset -v raw_chars pascal upper
r='\033[31m' #red
b='\033[34m' #blue
g='\033[32m' #green
d='\033[1m' #bold
s='\033[0m' #reset
out() { printf '%s\n' "$@"; }
__errex() {
fatal_string="${d}Fatal error [$r%s$s$d] on line $g%s$s$d in '$b%s$s$d':$s %s\n"
printf "${fatal_string}" \
"${1:-"?"}" \
"${2:-"?"}" \
"${3:-"undetermined script"}" \
"${4:-"undetermined error"}" >&2 ;
exit "${1:-1}"
}
alias die='__errex "$?" "${LINENO}" "$0"'
__outex() {
abandon_string="${d}Abandoning script '$b%s$s$d' at line $g%s$s$d with code [$r%s$s$d]:$s %s\n"
printf "${abandon_string}" \
"${1:-"undetermined script"}" \
"${2:-"?"}" \
"${3:-"?"}" \
"${4:-"undetermined reason"}" >&2 ;
exit "${3:-1}"
}
alias bye='__outex "$0" "${LINENO}" "$?"'
set_raw_chars() {
smash="$*"
raw_chars=
while [ -n "${smash}" ]; do
remains="${smash#?}"
raw_chars="${raw_chars}${smash%%"${remains}"} "
smash="${remains}"
done
}
set_pascal() {
set_upper() {
case "$*" in
a) upper="A" ;; b) upper="B" ;; c) upper="C" ;;
d) upper="D" ;; e) upper="E" ;; f) upper="F" ;;
g) upper="G" ;; h) upper="H" ;; i) upper="I" ;;
j) upper="J" ;; k) upper="K" ;; l) upper="L" ;;
m) upper="M" ;; n) upper="N" ;; o) upper="O" ;;
p) upper="P" ;; q) upper="Q" ;; r) upper="R" ;;
s) upper="S" ;; t) upper="T" ;; u) upper="U" ;;
v) upper="V" ;; w) upper="W" ;; x) upper="X" ;;
y) upper="Y" ;; z) upper="Z" ;; *) upper="$*" ;;
esac
}
set_upper "$1"
pascal="${upper}"
shift
while [ "$#" -gt 0 ]; do
if [ "$1" = "_" ]; then
shift
set_upper "$1"
pascal="${pascal}${upper}"
else
pascal="${pascal}$1"
fi
shift
done
}
## Initial checks
out "-- Checking elan default toolchain..."
elan toolchain list | tee /dev/tty | grep -qFe 'stable (default)' || {
out "----------------------------------------------" \
"Warning: default elan toolchain is not stable!" \
"Always install elan with the stable toolchain." \
"----------------------------------------------" \
"Continue anyway? " ;
read -r response || die "Unable to read response."
case "${response}" in
y|Y|yes|Yes|YES) : ;;
*) bye "rejecting toolchain." ;;
esac
}
grep -qE '^[[:alnum:]_]+$' <<NAME || die "invalid characters in project name."
$*
NAME
set_raw_chars "$*"
set_pascal ${raw_chars}
## Confirm project creation
out "-------------------------" \
"Current directory: ${PWD}" \
"Project name : $*" \
"Pascal name : ${pascal}" \
"-------------------------" \
"Is this ok? " ;
read -r response ||
die "Unable to read response."
case "${response}" in
y|Y|yes|Yes|YES) : ;;
*) bye "rejecting project names." ;;
esac
lake new "$*" math ||
die "command 'lake new' failed."
cd "$*" ||
die "cannot cd to new directory."
mv -f lakefile.lean lakefile.original
cat <<LAKEFILE >| lakefile.lean || die "unable to write new lakefile."
import Lake
open Lake DSL
package «$*» where
-- Settings applied to both builds and interactive editing
leanOptions := #[
⟨\`pp.unicode.fun, true⟩ -- pretty-prints \`fun a ↦ b\`
]
-- add any additional package configuration options here
lean_lib «${pascal}» where
/-!
mathlib ensures batteries, Cli, Qq, aesop, proofwidgets and importGraph
-/
require alloy from git "https://github.com/tydeu/lean4-alloy.git"
require mathlib from git "https://github.com/leanprover-community/mathlib4.git"
@[default_target]
lean_exe $* where
root := \`Main
LAKEFILE
out "-- Created new lakefile; if the build fails, check syntax compatibility." \
"-- The original file generated by lake is 'lakefile.original'." ;
out 'def main : IO Unit :=' ' IO.println "Clean main!"' >| Main.lean ||
die "failed to create Main.lean"
out "-- Directory ready; trying to build..."
## Try build
lake build &&
./.lake/build/bin/$*
exit