tydeu
|
4b9a765cfb
|
refactor PackageTarget -> ActivePackageTarget
|
2021-09-05 16:29:18 -04:00 |
|
tydeu
|
d4ba706198
|
refactor: purify BuildBin.lean
|
2021-09-05 15:37:16 -04:00 |
|
tydeu
|
92696d48f6
|
feat: use olean instead of lean hash for module targets
|
2021-09-05 01:01:40 -04:00 |
|
tydeu
|
720ecbd568
|
refactor: more cleanup (primarly Trace.lean)
|
2021-09-05 00:31:23 -04:00 |
|
tydeu
|
7129433066
|
fix: typo in foldArrayAsync
|
2021-09-04 20:41:03 -04:00 |
|
tydeu
|
3e1cdda87e
|
refactor: make PackageConfig take normal targets
|
2021-09-04 18:53:21 -04:00 |
|
tydeu
|
0a3457e973
|
refactor: minor cleanup / tweaks
|
2021-09-04 18:41:20 -04:00 |
|
tydeu
|
dba37698c8
|
refactor: rename LakeTrace to BuildTrace
|
2021-09-04 17:49:08 -04:00 |
|
tydeu
|
80416677d8
|
refactor: compute trace duing build
|
2021-09-04 17:45:56 -04:00 |
|
tydeu
|
2d3bec2209
|
feat: add proper CLI
|
2021-08-22 11:17:18 -04:00 |
|
tydeu
|
1825e095e1
|
refactore: rename ModuleM
|
2021-08-22 03:51:44 -04:00 |
|
tydeu
|
332af4c262
|
refactor: check hash after verifying module artifact exists
|
2021-08-22 03:40:09 -04:00 |
|
tydeu
|
4ce8716b99
|
feat: build and print-paths now build only oleans
|
2021-08-22 03:23:43 -04:00 |
|
tydeu
|
ac1cc9e62c
|
chore: cleanup
|
2021-08-22 03:06:33 -04:00 |
|
tydeu
|
80a9685164
|
refactor add ModuleTargetMap abbreviation
|
2021-08-22 00:16:18 -04:00 |
|
tydeu
|
ce1ee3c36d
|
refactor: move build failed message into runBuild
|
2021-08-22 00:07:17 -04:00 |
|
tydeu
|
43d1dfe72c
|
refactor: cleanup opaque target interfaces
|
2021-08-21 23:52:34 -04:00 |
|
tydeu
|
c843f0b112
|
chore: cleanup
|
2021-08-21 22:43:27 -04:00 |
|
tydeu
|
64634dbc32
|
refactor: change target abstraction (again)
|
2021-08-21 21:05:52 -04:00 |
|
tydeu
|
d12c4241bf
|
fix: use BuildM in PackageConfig
|
2021-08-21 20:17:48 -04:00 |
|
tydeu
|
56a78f6eeb
|
feat: use deps' extra lib targets when building parent bin
|
2021-08-20 01:48:10 -04:00 |
|
tydeu
|
8f7e32d09a
|
refactor: add build monad
|
2021-08-19 23:21:23 -04:00 |
|
tydeu
|
a371e181d5
|
refactor: more API tweaks
|
2021-08-19 12:13:29 -04:00 |
|
tydeu
|
8b74108f6e
|
refactor: remove FilesTarget
|
2021-08-19 12:05:44 -04:00 |
|
tydeu
|
28320f80ee
|
refactor: minor API tweaks
|
2021-08-19 12:05:28 -04:00 |
|
tydeu
|
0bfebc1975
|
refactor: reorganize Async.lean
|
2021-08-18 21:30:41 -04:00 |
|
tydeu
|
f9d6f57725
|
refactor: split Build into BuildModule and BuildPackage
|
2021-08-18 14:46:54 -04:00 |
|
tydeu
|
66a6246136
|
chore: fix typo
|
2021-08-18 12:48:58 -04:00 |
|
tydeu
|
81a84d21de
|
feat: add command to verify Lean version
|
2021-08-17 11:24:32 -04:00 |
|
tydeu
|
dd6634544d
|
misc: add shell scripts for timing Lake builds
|
2021-08-17 10:34:18 -04:00 |
|
tydeu
|
31abd420ad
|
chore: update Lean version
Some examples (ex. `hello`) may now segfault. See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Problems.20when.20updating.20Lean/near/249599195.
|
2021-08-17 10:33:15 -04:00 |
|
tydeu
|
d49c64453d
|
refactor: build with leanmake instead of leanpkg
|
2021-08-16 09:23:51 -04:00 |
|
tydeu
|
f977ee8b34
|
refactor: improve async abstraction
|
2021-08-15 20:41:55 -04:00 |
|
tydeu
|
2757e844dd
|
refactor: add trace abstraction
|
2021-08-15 20:13:17 -04:00 |
|
tydeu
|
c8b558a2d1
|
refactor: remove 'build' from Target/Trace/Task file names
|
2021-08-15 19:16:12 -04:00 |
|
tydeu
|
ddf02cb339
|
refactor: merge build target into lake target
|
2021-08-15 19:04:28 -04:00 |
|
tydeu
|
23dd052dc9
|
refactor: remove BuildTask
|
2021-08-15 17:14:13 -04:00 |
|
tydeu
|
c1f61d6716
|
feat add config setting for specificying extra lib targets
|
2021-08-15 16:12:45 -04:00 |
|
tydeu
|
4f75dd99d1
|
reefactor: improve async API
|
2021-08-09 05:04:38 -04:00 |
|
tydeu
|
d0fbc93143
|
refactor: improve Hash traces
|
2021-08-06 01:58:41 -04:00 |
|
tydeu
|
609ee22971
|
refactor: LeanTrace/Target -> LakeTrace/Target
|
2021-08-06 01:17:17 -04:00 |
|
tydeu
|
81d7511792
|
refactor: post-async Target API touch-ups
|
2021-08-06 00:44:46 -04:00 |
|
tydeu
|
859b04bf7f
|
refactor: generalize Target/ActiveTarget beyond IO
|
2021-08-05 00:45:50 -04:00 |
|
tydeu
|
aa1ca9c4b7
|
feat: improve Target API
|
2021-08-04 14:07:28 -04:00 |
|
tydeu
|
a541f2054e
|
refactor: IO BuildTarget task / protect pure
|
2021-08-04 01:31:47 -04:00 |
|
tydeu
|
ba52b36ef8
|
chore: more code cleanup
|
2021-08-01 18:46:48 -04:00 |
|
tydeu
|
3643b8e424
|
refactor: make Task and task a monad
|
2021-08-01 18:46:33 -04:00 |
|
tydeu
|
6a6afcd7c0
|
refactor: spawn ActiveBuildTarget from BuildTarget
|
2021-08-01 16:50:53 -04:00 |
|
tydeu
|
b8e85f40cd
|
refactor: move afterTarget* into ActiveBuildTarget
|
2021-08-01 15:40:11 -04:00 |
|
tydeu
|
2d78f4db36
|
feat: add non-activve targets
|
2021-08-01 15:17:43 -04:00 |
|