tydeu
4441662490
test: lake: tests/manifest -> tests/depTree
...
also clarify its difference distinction with `tests/clone`
2023-10-16 13:35:24 -04:00
tydeu
8db978bb10
chore: lake: fail if no error in tests/serve
2023-10-16 13:35:24 -04:00
tydeu
2a91d3cf68
fix: lake: casing in tests/order/clean.sh
2023-10-16 13:35:24 -04:00
David Thrane Christiansen
d15a0a4acb
chore: lake: explicit branch name in tests/clone
2023-10-16 09:29:31 +00:00
tydeu
f3de5eb1e8
feat: lake: --no-build to exit before a build
2023-10-13 14:42:58 +02:00
tydeu
42802f9788
feat: lake: postUpdate? + test
2023-10-13 02:31:06 -04:00
tydeu
275af93904
test: lake: show module with failed import
2023-10-12 22:16:04 -04:00
int-y1
ce4ae37c19
chore: fix more typos in comments
2023-10-08 14:37:34 -07:00
tydeu
1354fd9ccd
perf: do not detect lean's toolchain
...
use `ELAN_TOOLCHAIN` only
2023-09-21 18:52:52 -04:00
tydeu
3be4d74321
fix: lake: lowercase template exe name to avoid clash with lib
2023-09-14 02:15:37 -04:00
tydeu
65fa1e06b2
feat: lake: improve package templates
...
* add library directory
* add note on `supportInterpreter`
* use `where`-style configs
2023-09-14 02:15:37 -04:00
tydeu
473d4c51ad
feat: lake: better native object tracing
...
* `weakLeanc/LinkArgs` for libs/mods/exes
* `weakArgs`/``extraDepTrace` for `buildO`
* include Lean trace when compiler is part of Lean toolchain
* do not include system-dependent file paths (e.g., `-I`) in dep trace
2023-09-14 02:15:37 -04:00
tydeu
becc6fdb0e
feat: lake: detect Elan install and Elan toolchain
2023-09-14 02:15:37 -04:00
tydeu
7b9d8a04c2
feat: lake: maintain order of libs and deps
...
provides a well-defined selection order when decls overlap
2023-09-14 02:15:37 -04:00
tydeu
522ea723ad
fix: lake: dep URL match check in updateGitRepo
...
see 6176fdba9e (r125905901)
2023-09-14 02:15:37 -04:00
tydeu
cfe4db16ea
test: lake: check warnings in tests/clone
...
tests leanprover/lean4#2427
2023-09-06 17:35:59 -04:00
tydeu
2e726f5f5a
test: lake: give issue tests meaningful names
2023-09-06 17:35:59 -04:00
tydeu
8c4811a300
test: lake: merge 49 and 116 into tests/serve
2023-09-06 17:35:59 -04:00
tydeu
398c131620
test: lake: merge tests/102 into globs
2023-09-06 17:35:59 -04:00
tydeu
9136309e59
test: lake: move examples/init to tests
2023-09-06 17:35:59 -04:00
tydeu
bb09efe1c4
test: lake: rename test to tests
...
(for consistency with Lean)
2023-09-06 17:35:59 -04:00
