tydeu
|
333a86ef5f
|
fix: typing mistakes with CliMethodsRef + cleanup
|
2021-10-24 17:34:40 -04:00 |
|
tydeu
|
e006f8534d
|
feat: add supportInterpreter config setting
also don't use `--export-all` on Windows anymore
|
2021-10-23 16:16:09 -04:00 |
|
tydeu
|
168ec3d178
|
perf: cache lean exe trace in BuildM
|
2021-10-23 14:36:37 -04:00 |
|
tydeu
|
20788e8237
|
refactor: separate module olean and c traces
|
2021-10-23 14:02:31 -04:00 |
|
tydeu
|
74276dd024
|
refactor: update ofByteArray with new primitives
also rename `getFileHash` to `computeFileHash`
|
2021-10-23 11:34:01 -04:00 |
|
tydeu
|
521311292d
|
chore: bump Lean version
|
2021-10-23 11:04:51 -04:00 |
|
tydeu
|
738425b0b1
|
ci: mssing $
|
2021-10-20 16:46:03 -04:00 |
|
tydeu
|
29975edb0e
|
ci: use matrix OS for build artifact name
|
2021-10-20 16:44:54 -04:00 |
|
tydeu
|
7cbde2c852
|
ci: switch back to homebrew on macOS
|
2021-10-19 11:36:36 -04:00 |
|
tydeu
|
c6f6eec4c5
|
fix; leanmake build
|
2021-10-19 11:30:24 -04:00 |
|
tydeu
|
aa3f453ebf
|
refactor: cleanup trace code some
|
2021-10-18 19:38:32 -04:00 |
|
tydeu
|
ffd5bc0f69
|
refactor: narrow Lean imports
|
2021-10-18 18:01:31 -04:00 |
|
tydeu
|
bfedab0f9b
|
feat: build C files in print-paths if facet is not oleans
|
2021-10-18 15:21:43 -04:00 |
|
tydeu
|
4d66b6e4e2
|
fix: ci: don't use hombrew for MacOS (for now)
Reason: it is missing `lake` (see https://github.com/Homebrew/homebrew-core/pull/87486)
|
2021-10-18 13:40:50 -04:00 |
|
tydeu
|
44cc860c82
|
fix: ci: use elan's lake to build (for now)
Reason: `leanmake` build is broken due to bad dep inference
|
2021-10-18 13:27:58 -04:00 |
|
tydeu
|
53ad51e984
|
fix: correct the lake lib location of a co-located lake and lean
|
2021-10-18 12:39:30 -04:00 |
|
tydeu
|
e9443705d5
|
feat: include hash of lean in module traces
closes leanprover/lake#23
|
2021-10-18 12:11:56 -04:00 |
|
tydeu
|
d9f53dfec9
|
refactor: replace leanpkg.toml with a lakefile.lean + build reorg
|
2021-10-17 13:52:01 -04:00 |
|
tydeu
|
b558536129
|
feat: add basic lake server CLI
|
2021-10-13 15:31:49 -04:00 |
|
tydeu
|
4eec17c876
|
chore: use return at examples/scripts
|
2021-10-13 14:47:57 -04:00 |
|
tydeu
|
1074aaa5fa
|
chore: fix hasModule error message at parseTargetBaseSpec
|
2021-10-10 12:52:49 -04:00 |
|
tydeu
|
b8b3f01c96
|
feat: add option to specify the lean used by Lake
also:
* support `=` for long CLI options
* cleanup some typos in `InstallPath`
|
2021-10-10 12:37:00 -04:00 |
|
tydeu
|
15a2981804
|
feat: new build CLI
|
2021-10-09 19:24:28 -04:00 |
|
tydeu
|
88af2ca4b7
|
refactor: reorg build package code
|
2021-10-09 18:48:53 -04:00 |
|
tydeu
|
d494626de6
|
chore: use Json.compress at print-paths
Reason: server expects JSON to be a single line
|
2021-10-09 12:04:08 -04:00 |
|
tydeu
|
ae01b5d586
|
chore: use c++ not cc at examples/fffi
|
2021-10-09 11:26:21 -04:00 |
|
tydeu
|
8635ce279b
|
refactor: use LeanPaths in print-paths
|
2021-10-08 21:00:42 -04:00 |
|
tydeu
|
b2822ffab1
|
chore: bump Lean version
|
2021-10-08 20:58:53 -04:00 |
|
tydeu
|
427cb0fc7c
|
feat: add inputFileTarget util
|
2021-10-08 15:26:07 -04:00 |
|
tydeu
|
85efdb159a
|
test: expand examples/ffi to use getLeanIncludeDir
|
2021-10-08 15:20:23 -04:00 |
|
tydeu
|
8a06d4f529
|
feat: introduce Workspace which is shared across a pkg and its deps
|
2021-10-08 14:09:05 -04:00 |
|
tydeu
|
7a3aadd005
|
feat: add utils for constructing file targets with deps
|
2021-10-08 12:58:10 -04:00 |
|
tydeu
|
b3b7aa02d1
|
fix: wait for deps to build on a bare print-paths
|
2021-10-07 18:30:52 -04:00 |
|
tydeu
|
2e5c7c02f1
|
refactor: CLI code tweaks
|
2021-10-07 14:59:00 -04:00 |
|
tydeu
|
1d20cbd3d6
|
refacttor: check LEAN_SYSROOT rather than LEAN_HOME for Lean
|
2021-10-07 14:04:18 -04:00 |
|
tydeu
|
9700208501
|
feat: have print-paths exit silently with code 2 if config missing
|
2021-10-07 12:40:26 -04:00 |
|
tydeu
|
6cfbd90426
|
refactor: always pass -O3 and -DNDEBUG when building Lean o files
also add `more` prefix to `leanArgs`/`leancArgs`/`linkArgs`
closes leanprover/lake#19
|
2021-10-06 21:07:56 -04:00 |
|
tydeu
|
e171925991
|
chore: update Lean version
fixes leanprover/lake#21
|
2021-10-06 20:43:36 -04:00 |
|
tydeu
|
0e7a2bae8e
|
refactor: clean up CLI code some
|
2021-10-06 20:06:03 -04:00 |
|
tydeu
|
429386c4c0
|
refactor: update print-paths JSON format to match server
|
2021-10-06 17:52:22 -04:00 |
|
tydeu
|
0f2d6c7fdd
|
feat: use detected Lean install to build packages
|
2021-10-06 17:38:57 -04:00 |
|
tydeu
|
c32cd22504
|
feat: store detected Lean/Lake install in BuildContext
includes new `getLeanIncludeDir` for `BuildM` (leanprover/lake#18)
|
2021-10-06 17:01:52 -04:00 |
|
tydeu
|
0196cbe6a3
|
refactor: move build execution into CLI
|
2021-10-06 16:27:49 -04:00 |
|
tydeu
|
93cc196b10
|
chore: minor code cleanup
|
2021-10-06 15:22:19 -04:00 |
|
tydeu
|
3bcd18a1c6
|
refactor: generalize Lean/Lake installation detection
|
2021-10-05 20:00:30 -04:00 |
|
tydeu
|
4c0734b5f1
|
feat: use hash traces for o file, static lib, and bin targets
Also rename `.hash` file to `.trace` and add a `package-bootstrap` make job
|
2021-10-04 19:08:22 -04:00 |
|
tydeu
|
ae144112be
|
refactor: generalize checkModuleTrace
|
2021-10-04 18:30:24 -04:00 |
|
tydeu
|
e906f39201
|
refactor: cleanup Compile.lean
|
2021-10-04 17:51:47 -04:00 |
|
tydeu
|
a9b87adbeb
|
feat: print-paths as a JSON object
|
2021-10-04 12:50:57 -04:00 |
|
tydeu
|
b2acab81d4
|
refactor: output print-paths build info to stderr
|
2021-10-04 12:27:14 -04:00 |
|