-
Notifications
You must be signed in to change notification settings - Fork 80
/
main.lean
316 lines (256 loc) · 11.8 KB
/
main.lean
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
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
/-
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Gabriel Ebner
-/
import leanpkg.resolve leanpkg.git
namespace leanpkg
def write_file (fn : string) (cnts : string) (mode := io.mode.write) : io unit := do
h ← io.mk_file_handle fn io.mode.write,
io.fs.write h cnts.to_char_buffer,
io.fs.close h
def read_manifest : io manifest := do
m ← manifest.from_file leanpkg_toml_fn,
when (m.lean_version ≠ lean_version_string) $
io.print_ln $ "\nWARNING: Lean version mismatch: installed version is " ++ lean_version_string
++ ", but package requires " ++ m.lean_version ++ "\n",
return m
def write_manifest (d : manifest) (fn := leanpkg_toml_fn) : io unit :=
write_file fn (repr d)
-- TODO(gabriel): implement a cross-platform api
def get_dot_lean_dir : io string := do
some home ← io.env.get "HOME" | io.fail "environment variable HOME is not set",
return $ home ++ "/.lean"
def mk_path_file : ∀ (paths : list string), string
| [] := "builtin_path\n"
| (x :: xs) := mk_path_file xs ++ "path " ++ x ++ "\n"
def configure : io unit := do
d ← read_manifest,
io.put_str_ln $ "configuring " ++ d.name ++ " " ++ d.version,
when (d.path ≠ some "src") $ io.put_str_ln "WARNING: leanpkg configurations not specifying `path = \"src\"` are deprecated.",
assg ← solve_deps d,
path_file_cnts ← mk_path_file <$> construct_path assg,
write_file "leanpkg.path" path_file_cnts
def make (lean_args : list string) : io unit := do
manifest ← read_manifest,
exec_cmd {
cmd := "lean",
args := (match manifest.timeout with some t := ["-T", repr t] | none := [] end) ++
["--make"] ++ manifest.effective_path ++ lean_args,
env := [("LEAN_PATH", none)]
}
def build (lean_args : list string) := configure >> make lean_args
def make_test (lean_args : list string) : io unit :=
exec_cmd { cmd := "lean", args := ["--make", "test"] ++ lean_args, env := [("LEAN_PATH", none)] }
def test (lean_args : list string) := build lean_args >> make_test lean_args
def init_gitignore_contents :=
"*.olean
/_target
/leanpkg.path
"
def init_pkg (n : string) (from_new : bool) : io unit := do
write_manifest { name := n, path := "src", version := "0.1" } leanpkg_toml_fn,
src_ex ← io.fs.dir_exists "src",
when (¬src_ex) (do
when ¬from_new $ io.put_str_ln "Move existing .lean files into the 'src' folder.",
io.fs.mkdir "src" >> return ()),
write_file ".gitignore" init_gitignore_contents io.mode.append,
git_ex ← io.fs.dir_exists ".git",
when (¬git_ex) (do {
exec_cmd {cmd := "git", args := ["init", "-q"]},
when (upstream_git_branch ≠ "master") $
exec_cmd {cmd := "git", args := ["checkout", "-b", upstream_git_branch]}
} <|> io.print_ln "WARNING: failed to initialize git repository"),
configure
def init (n : string) := init_pkg n false
-- TODO(gabriel): windows
def basename (s : string) : string :=
s.fold "" $ λ s c, if c = '/' then "" else s.str c
def add_dep_to_manifest (dep : dependency) : io unit := do
d ← read_manifest,
let d' := { d with dependencies := d.dependencies.filter (λ old_dep, old_dep.name ≠ dep.name) ++ [dep] },
write_manifest d'
def strip_dot_git (url : string) : string :=
if url.backn 4 = ".git" then url.popn_back 4 else url
def looks_like_git_url (dep : string) : bool :=
':' ∈ dep.to_list
def parse_add_dep (dep : string) (branch : option string) : io dependency :=
if looks_like_git_url dep then
pure { name := basename (strip_dot_git dep), src := source.git dep (git_default_revision branch) branch }
else do
ex ← io.fs.dir_exists dep,
if ex then match branch with
| some branch := io.fail sformat!"extraneous trailing path argument '{branch}'"
| none := pure { name := basename dep, src := source.path dep }
end
else do
[user, repo] ← pure $ dep.split (= '/')
| io.fail sformat!"path '{dep}' does not exist",
pure { name := repo, src := source.git sformat!"https://github.com/{user}/{repo}" (git_default_revision branch) branch }
def absolutize_dep (dep : dependency) : io dependency :=
match dep.src with
| source.path p := do
cwd ← io.env.get_cwd,
pure {src := source.path (resolve_dir p cwd), ..dep}
| _ := pure dep
end
def parse_install_dep (dep : string) (branch : option string) : io dependency := do
dep ← parse_add_dep dep none,
dep ← absolutize_dep dep,
dot_lean_dir ← get_dot_lean_dir,
io.fs.mkdir dot_lean_dir tt,
let user_toml_fn := dot_lean_dir ++ "/" ++ leanpkg_toml_fn,
ex ← io.fs.file_exists user_toml_fn,
when (¬ ex) $ write_manifest {
name := "_user_local_packages",
version := "1"
} user_toml_fn,
change_dir dot_lean_dir,
return dep
def fixup_git_version (dir : string) : ∀ (src : source), io source
| (source.git url _ _) := do
rev ← git_head_revision dir,
return $ source.git url rev none
| src := return src
def add (dep : dependency) : io unit := do
(_, assg) ← (materialize "." dep).run assignment.empty,
some downloaded_path ← return (assg.find dep.name),
manif ← manifest.from_file (downloaded_path ++ "/" ++ leanpkg_toml_fn),
src ← fixup_git_version downloaded_path dep.src,
let dep := { dep with name := manif.name, src := src },
add_dep_to_manifest dep,
configure
def new (dir : string) := do
ex ← io.fs.dir_exists dir,
when ex $ io.fail $ "directory already exists: " ++ dir,
io.fs.mkdir dir tt,
change_dir dir,
init_pkg (basename dir) true
def upgrade_dep (assg : assignment) (d : dependency) : io dependency :=
match d.src with
| (source.git url rev branch) := (do
some path ← return (assg.find d.name) | io.fail "unresolved dependency",
new_rev ← git_latest_origin_revision path branch,
return {d with src := source.git url new_rev branch})
<|> return d
| _ := return d
end
def upgrade := do
m ← read_manifest,
assg ← solve_deps m,
ds' ← m.dependencies.mmap (upgrade_dep assg),
write_manifest {m with dependencies := ds'},
configure
def usage :=
"Lean package manager, version " ++ ui_lean_version_string ++ "
Usage: leanpkg <command>
configure download dependencies
build [-- <lean-args>] download dependencies and build *.olean files
test [-- <lean-args>] download dependencies, build *.olean files, and run test files
new <dir> create a Lean package in a new directory
init <name> create a Lean package in the current directory
add <url> [branch] add a dependency from a git repository (uses latest upstream revision)
add <dir> add a local dependency
upgrade upgrade all git dependencies to the latest upstream version
install <url> [branch] install a user-wide package from git
install <dir> install a user-wide package from a local directory
dump print the parsed leanpkg.toml file (for debugging)
See `leanpkg help <command>` for more information on a specific command."
def main : ∀ (cmd : string) (leanpkg_args lean_args : list string), io unit
| "configure" [] [] := configure
| "build" _ lean_args := build lean_args
| "test" _ lean_args := test lean_args
| "new" [dir] [] := new dir
| "init" [name] [] := init name
| "add" [dep] [] := parse_add_dep dep none >>= add
| "add" [dep] [branch] := parse_add_dep dep branch >>= add
| "upgrade" [] [] := upgrade
| "install" [dep] [] := parse_install_dep dep none >>= add >> build []
| "install" [dep] [branch] := parse_install_dep dep branch >>= add >> build []
| "dump" [] [] := read_manifest >>= io.print_ln ∘ repr
| "help" ["configure"] [] := io.print_ln "Download dependencies
Usage:
leanpkg configure
This command sets up the `_target/deps` directory and the `leanpkg.path` file.
For each (transitive) git dependency, the specified commit is checked out
into a sub-directory of `_target/deps`. If there are dependencies on multiple
versions of the same package, the version materialized is undefined.
The `leanpkg.path` file used to resolve Lean imports is populated with paths
to the `src` directories of all (transitive) dependencies. No copy is made
of local dependencies."
| "help" ["build"] [] := io.print_ln "Download dependencies and build *.olean files
Usage:
leanpkg build [-- <lean-args>]
This command invokes `leanpkg configure` followed by
`lean --make src <lean-args>`, building the package's Lean files as well as
(transitively) imported files of dependencies. If defined, the `package.timeout`
configuration value is passed to Lean via its `-T` parameter."
| "help" ["test"] [] := io.print_ln "Download dependencies, build *.olean files, and run test files
Usage:
leanpkg test [-- <lean-args>]
This command invokes `leanpkg build <lean-args>` followed by
`lean --make test <lean-args>`, executing the package's test files. A failed
test should generate a Lean error message, which makes this command return a
non-zero exit code."
| "help" ["add"] [] := io.print_ln sformat!"Add a dependency
Usage:
leanpkg add <local-path>
leanpkg add <git-url>
leanpkg add <github-user>/<github-repo>
Examples:
leanpkg add ../mathlib
leanpkg add https://github.com/leanprover/mathlib
leanpkg add leanprover/mathlib
This command adds the specified local or git dependency, then calls
`leanpkg configure`. For git dependencies, the pinned commit is
the head of the branch `lean-<version>` (e.g. `lean-3.3.0`) on stable
releases of Lean, or else `master` (current branch: {upstream_git_branch})."
| "help" ["new"] [] := io.print_ln "Create a new Lean package in a new directory
Usage:
leanpkg new <path>/.../<name>
This command creates a new Lean package named '<name>' in a new directory
`<path>/.../<name>`. A new git repository is initialized to the branch name
expected by `leanpkg add` (see `leanpkg help add`).
For converting an existing directory into a Lean package, use `leanpkg init`."
| "help" ["init"] [] := io.print_ln "Create a new Lean package in the current directory
Usage:
leanpkg init <name>
This command creates a new Lean package with the given name in the current
directory. Existing Lean source files should be moved into the new `src`
directory."
| "help" ["upgrade"] [] := io.print_ln "Upgrade all git dependencies to the latest upstream version
Usage:
leanpkg upgrade
This command fetches the remote repositories of all git dependencies and updates
the pinned commits to the head of the respective branch (see
`leanpkg help add`)."
| "help" ["install"] [] := io.print_ln "Install a user-wide package
Usage:
leanpkg install <local-path>
leanpkg install <git-url>
leanpkg install <github-user>/<github-repo>
This command adds a dependency to a user-wide \"meta\" package in `~/.lean`.
For files not part of a Lean package, Lean falls back to the core library
and this meta package for import resolution.
For removing or upgrading user-wide dependencies, you currently have to change
into `~/.lean` yourself and edit the leanpkg.toml file or execute
`leanpkg upgrade`, respectively."
| "help" _ [] := io.print_ln usage
| _ _ _ := io.fail usage
private def split_cmdline_args_core : list string → list string × list string
| [] := ([], [])
| (arg::args) := if arg = "--"
then ([], args)
else match split_cmdline_args_core args with
| (outer_args, inner_args) := (arg::outer_args, inner_args)
end
def split_cmdline_args : list string → io (string × list string × list string)
| [] := io.fail usage
| [cmd] := return (cmd, [], [])
| (cmd::rest) := match split_cmdline_args_core rest with
| (outer_args, inner_args) := return (cmd, outer_args, inner_args)
end
end leanpkg
def main : io unit :=
do (cmd, outer_args, inner_args) ← io.cmdline_args >>= leanpkg.split_cmdline_args,
leanpkg.main cmd outer_args inner_args