tydeu
|
e9443705d5
|
feat: include hash of lean in module traces
closes leanprover/lake#23
|
2021-10-18 12:11:56 -04:00 |
|
tydeu
|
88af2ca4b7
|
refactor: reorg build package code
|
2021-10-09 18:48:53 -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
|
0f2d6c7fdd
|
feat: use detected Lean install to build packages
|
2021-10-06 17:38:57 -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
|
3b78652547
|
refactor: prefer build rather than fetch terminology
|
2021-09-27 02:50:45 -04:00 |
|
tydeu
|
032be7ee2e
|
refactor: generalize buildRBTop
|
2021-09-27 02:40:24 -04:00 |
|
tydeu
|
5b37f1c5c5
|
feat: split moduleRoot into libRoots and libGlobs
Reason: provide finer grain control over library modules
|
2021-09-23 21:04:29 -04:00 |
|
tydeu
|
8601c0fe78
|
refactor: purify BuildModule somewhat + associated cleanup
|
2021-09-05 18:05:45 -04:00 |
|
tydeu
|
6863bb8095
|
refactor: ModuleTarget -> ActiveModuleTarget
|
2021-09-05 16:30:28 -04:00 |
|
tydeu
|
92696d48f6
|
feat: use olean instead of lean hash for module targets
|
2021-09-05 01:01:40 -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
|
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
|
80a9685164
|
refactor add ModuleTargetMap abbreviation
|
2021-08-22 00:16:18 -04:00 |
|
tydeu
|
43d1dfe72c
|
refactor: cleanup opaque target interfaces
|
2021-08-21 23:52:34 -04:00 |
|
tydeu
|
8f7e32d09a
|
refactor: add build monad
|
2021-08-19 23:21:23 -04:00 |
|
tydeu
|
f9d6f57725
|
refactor: split Build into BuildModule and BuildPackage
|
2021-08-18 14:46:54 -04:00 |
|