-
Notifications
You must be signed in to change notification settings - Fork 350
/
Leanpkg.lean
229 lines (197 loc) · 8.71 KB
/
Leanpkg.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
/-
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gabriel Ebner, Sebastian Ullrich
-/
import Leanpkg.Resolve
import Leanpkg.Git
import Leanpkg.Build
open System
namespace Leanpkg
def readManifest : IO Manifest := do
let m ← Manifest.fromFile leanpkgTomlFn
if m.leanVersion ≠ leanVersionString then
IO.eprintln $ "\nWARNING: Lean version mismatch: installed version is " ++ leanVersionString
++ ", but package requires " ++ m.leanVersion ++ "\n"
return m
def writeManifest (manifest : Lean.Syntax) (fn : FilePath) : IO Unit := do
IO.FS.writeFile fn manifest.reprint.get!
def lockFileName : System.FilePath := ⟨".leanpkg-lock"⟩
partial def withLockFile (x : IO α) : IO α := do
acquire
try
x
finally
IO.FS.removeFile lockFileName
where
acquire (firstTime := true) :=
try
-- TODO: lock file should ideally contain PID
if !System.Platform.isWindows then
discard <| IO.FS.Handle.mkPrim lockFileName "wx"
else
-- `x` mode doesn't seem to work on Windows even though it's listed at
-- https://docs.microsoft.com/en-us/cpp/c-runtime-library/reference/fopen-wfopen?view=msvc-160
-- ...? Let's use the slightly racy approach then.
if ← lockFileName.pathExists then
throw <| IO.Error.alreadyExists none 0 ""
discard <| IO.FS.Handle.mk lockFileName IO.FS.Mode.write
catch
| IO.Error.alreadyExists .. => do
if firstTime then
IO.eprintln s!"Waiting for prior leanpkg invocation to finish... (remove '{lockFileName}' if stuck)"
IO.sleep (ms := 300)
acquire (firstTime := false)
| e => throw e
def getRootPart (pkg : FilePath := ".") : IO Lean.Name := do
let entries ← pkg.readDir
match entries.filter (FilePath.extension ·.fileName == "lean") with
| #[rootFile] => FilePath.withExtension rootFile.fileName "" |>.toString
| #[] => throw <| IO.userError s!"no '.lean' file found in {← IO.FS.realPath "."}"
| _ => throw <| IO.userError s!"{← IO.FS.realPath "."} must contain a unique '.lean' file as the package root"
structure Configuration :=
leanPath : String
leanSrcPath : String
moreDeps : List FilePath
def configure : IO Configuration := do
let d ← readManifest
IO.eprintln $ "configuring " ++ d.name ++ " " ++ d.version
let assg ← solveDeps d
let paths ← constructPath assg
let mut moreDeps := [leanpkgTomlFn]
for path in paths do
unless path == FilePath.mk "." / "." do
-- build recursively
-- TODO: share build of common dependencies
execCmd {
cmd := (← IO.appPath).toString
cwd := path
args := #["build"]
}
moreDeps := (path / Build.buildPath / (← getRootPart path).toString |>.withExtension "olean") :: moreDeps
return {
leanPath := SearchPath.toString <| paths.map (· / Build.buildPath)
leanSrcPath := SearchPath.toString paths
moreDeps
}
def execMake (makeArgs : List String) (cfg : Build.Config) : IO Unit := withLockFile do
let manifest ← readManifest
let leanArgs := (match manifest.timeout with | some t => ["-T", toString t] | none => []) ++ cfg.leanArgs
let mut spawnArgs := {
cmd := "sh"
cwd := manifest.effectivePath
args := #["-c", s!"\"{← IO.appDir}/leanmake\" PKG={cfg.pkg} LEAN_OPTS=\"{" ".intercalate leanArgs}\" LEAN_PATH=\"{cfg.leanPath}\" {" ".intercalate makeArgs} MORE_DEPS+=\"{" ".intercalate (cfg.moreDeps.map toString)}\" >&2"]
}
execCmd spawnArgs
def buildImports (imports : List String) (leanArgs : List String) : IO Unit := do
unless ← leanpkgTomlFn.pathExists do
return
let manifest ← readManifest
let cfg ← configure
let imports := imports.map (·.toName)
let root ← getRootPart
let localImports := imports.filter (·.getRoot == root)
if localImports != [] then
let buildCfg : Build.Config := { pkg := root, leanArgs, leanPath := cfg.leanPath, moreDeps := cfg.moreDeps }
if ← FilePath.pathExists "Makefile" then
let oleans := localImports.map fun i => Lean.modToFilePath "build" i "olean" |>.toString
execMake oleans buildCfg
else
Build.buildModules buildCfg localImports
IO.println cfg.leanPath
IO.println cfg.leanSrcPath
def build (makeArgs leanArgs : List String) : IO Unit := do
let cfg ← configure
let root ← getRootPart
let buildCfg : Build.Config := { pkg := root, leanArgs, leanPath := cfg.leanPath, moreDeps := cfg.moreDeps }
if makeArgs != [] || (← FilePath.pathExists "Makefile") then
execMake makeArgs buildCfg
else
Build.buildModules buildCfg [root]
def initGitignoreContents :=
"/build
"
def initPkg (n : String) (fromNew : Bool) : IO Unit := do
IO.FS.writeFile leanpkgTomlFn s!"[package]
name = \"{n}\"
version = \"0.1\"
lean_version = \"{leanVersionString}\"
"
IO.FS.writeFile ⟨s!"{n.capitalize}.lean"⟩ "def main : IO Unit :=
IO.println \"Hello, world!\"
"
let h ← IO.FS.Handle.mk ⟨".gitignore"⟩ IO.FS.Mode.append (bin := false)
h.putStr initGitignoreContents
unless ← System.FilePath.isDir ⟨".git"⟩ do
(do
execCmd {cmd := "git", args := #["init", "-q"]}
unless upstreamGitBranch = "master" do
execCmd {cmd := "git", args := #["checkout", "-B", upstreamGitBranch]}
) <|> IO.eprintln "WARNING: failed to initialize git repository"
def init (n : String) := initPkg n false
def usage :=
"Lean package manager, version " ++ uiLeanVersionString ++ "
Usage: leanpkg <command>
init <name> create a Lean package in the current directory
configure download and build dependencies
build [<args>] configure and build *.olean files
See `leanpkg help <command>` for more information on a specific command."
def main : (cmd : String) → (leanpkgArgs leanArgs : List String) → IO Unit
| "init", [Name], [] => init Name
| "configure", [], [] => discard <| configure
| "print-paths", leanpkgArgs, leanArgs => buildImports leanpkgArgs leanArgs
| "build", makeArgs, leanArgs => build makeArgs leanArgs
| "help", ["configure"], [] => IO.println "Download dependencies
Usage:
leanpkg configure
This command sets up the `build/deps` directory.
For each (transitive) git dependency, the specified commit is checked out
into a sub-directory of `build/deps`. If there are dependencies on multiple
versions of the same package, the version materialized is undefined. No copy
is made of local dependencies."
| "help", ["build"], [] => IO.println "download dependencies and build *.olean files
Usage:
leanpkg build [<leanmake-args>] [-- <lean-args>]
This command invokes `leanpkg configure` followed by `leanmake <leanmake-args> LEAN_OPTS=<lean-args>`.
If defined, the `package.timeout` configuration value is passed to Lean via its `-T` parameter.
If no <lean-args> are given, only .olean files will be produced in `build/`. If `lib` or `bin`
is passed instead, the extracted C code is compiled with `c++` and a static library in `build/lib`
or an executable in `build/bin`, respectively, is created. `leanpkg build bin` requires a declaration
of name `main` in the root namespace, which must return `IO Unit` or `IO UInt32` (the exit code) and
may accept the program's command line arguments as a `List String` parameter.
NOTE: building and linking dependent libraries currently has to be done manually, e.g.
```
$ (cd a; leanpkg build lib)
$ (cd b; leanpkg build bin LINK_OPTS=../a/build/lib/libA.a)
```"
| "help", ["init"], [] => IO.println "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."
| "help", _, [] => IO.println usage
| _, _, _ => throw <| IO.userError usage
private def splitCmdlineArgsCore : List String → List String × List String
| [] => ([], [])
| (arg::args) => if arg == "--"
then ([], args)
else
let (outerArgs, innerArgs) := splitCmdlineArgsCore args
(arg::outerArgs, innerArgs)
def splitCmdlineArgs : List String → IO (String × List String × List String)
| [] => throw <| IO.userError usage
| [cmd] => return (cmd, [], [])
| (cmd::rest) =>
let (outerArgs, innerArgs) := splitCmdlineArgsCore rest
return (cmd, outerArgs, innerArgs)
end Leanpkg
def main (args : List String) : IO UInt32 := do
try
Lean.enableInitializersExecution
Lean.initSearchPath none -- HACK
let (cmd, outerArgs, innerArgs) ← Leanpkg.splitCmdlineArgs args
Leanpkg.main cmd outerArgs innerArgs
pure 0
catch e =>
IO.eprintln e -- avoid "uncaught exception: ..."
pure 1