mhuisi
7eb3eb189f
chore: add new issue templates
2023-09-15 14:24:21 +02:00
tydeu
be97757982
chore: lake: code cleanup
...
* remove MTime `checkIfNewer`
* remove unnecessary `@[noinline]`
* inline `MainM` combinators
2023-09-14 02:15:37 -04:00
tydeu
3be4d74321
fix: lake: lowercase template exe name to avoid clash with lib
2023-09-14 02:15:37 -04:00
tydeu
9088df4c57
doc: lake: add pkg org info to README + other tweaks
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
be2eef5f3b
feat: lake: better cloud release management
...
* step logging for cloud release fetching
* do not include cloud release bundle in trace
* `Package.afterReleaseSync/Async` utilities
* also cleanup `Package.recComputeDeps`
2023-09-14 02:15:37 -04:00
tydeu
0bb6bcf24c
feat: lake: add upgrade and exec CLI aliases
2023-09-14 02:15:37 -04:00
tydeu
5983abcf78
fix: lake: use manifest opts
...
specifically, union manifest and config opts (preferring manifest)
2023-09-14 02:15:37 -04:00
tydeu
3f4a9dc9a1
feat: lake: better manifest-related error messages
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
e96b338cd9
feat: lake run <s> for s in any pkg
2023-09-14 02:15:37 -04:00
tydeu
113caf73fa
fix: lake: reconfigure if toolchain changes
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
Scott Morrison
c318d5817d
feat: allow configuring occs in rw
2023-09-13 12:03:18 -07:00
Joachim Breitner
09b9fdbdc3
chore: Do not hide stage0/src/stdlib_flags.h from diffs
2023-09-13 19:29:25 +02:00
Sebastian Ullrich
c2a5730bc9
chore: update stage0
2023-09-13 17:45:54 +02:00
Sebastian Ullrich
e9d60e143a
perf: avoid allocation in mkUnexpectedTokenErrors
2023-09-12 11:42:24 +02:00
Sebastian Ullrich
aab0e382c8
perf: inline ParserState.hasError
2023-09-12 11:42:24 +02:00
Sebastian Ullrich
241430aa03
perf: avoid calculating position, revert building unexpected message in mkUnexpectedTokenErrors
2023-09-12 11:42:24 +02:00
Sebastian Ullrich
c67686132a
feat: include unexpected token in error message
2023-09-12 11:42:24 +02:00
Sebastian Ullrich
e580c903e6
feat: adjust message range on unexpected token error
2023-09-12 11:42:24 +02:00
Sebastian Ullrich
6c0baf4aed
feat: support reporting range for parser errors, report ranges for expected token errors
2023-09-12 11:42:24 +02:00
Sebastian Ullrich
f4fc8b3e15
refactor: parser error setters
2023-09-12 11:42:24 +02:00
mhuisi
3aa1cfccea
doc: update quickstart doc for release
2023-09-08 16:39:55 +02:00
Jannis Limperg
13ca443f05
fix: simp: include class projections in UsedSimps ( #2489 )
...
* fix: simp: include class projections in UsedSimps
Fixes #2488
2023-09-07 08:54:00 +10: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
Mario Carneiro
2037094f8c
doc: document all parser aliases ( #2499 )
2023-09-06 09:02:25 +00:00
Marcus Rossel
84bf315ac8
doc: fix comment for Unit
2023-09-05 07:52:06 +01:00
Scott Morrison
66e1472c7e
chore: in nightly release notes, look for changes since last nightly
2023-09-01 11:08:18 +01:00
Scott Morrison
77600c56b6
chore: base lean-pr-testing-NNNN branches off nightly-testing ( #2503 )
2023-09-01 05:43:13 +00:00
Jannis Limperg
9a262d7cef
fix: simpGoal reports incomplete UsedSimps ( #2487 )
2023-09-01 10:20:49 +10:00
Mario Carneiro
fec3575aaf
fix: 0-arg functions in C need f(void)
2023-08-31 15:39:47 -04:00
tydeu
4cc1ca7a58
chore: lake: update tests
2023-08-31 15:37:33 -04:00
tydeu
5f77e70d27
feat: lake: save elaborated config as an olean
2023-08-31 15:37:33 -04:00
tydeu
926663505e
chore: split up & simplify importModules
2023-08-31 15:37:33 -04:00
Scott Morrison
b2119313bd
feat: add toolchain-available labels to PRs ( #2492 )
2023-08-31 08:36:32 +00:00
Scott Morrison
7de335c661
fix: create a mathlib branch for each Lean PR ( #2494 )
2023-08-31 05:48:24 +00:00
Scott Morrison
c4540f75b8
chore: create a mathlib branch for each Lean PR ( #2473 )
...
* chore: create a mathlib branch for each Lean PR
* use existing branch if present
2023-08-31 13:24:41 +10:00
Scott Morrison
0901e062eb
feat: when making PR releases, only download necessary artifacts ( #2474 )
2023-08-31 12:52:22 +10:00
tydeu
a0440ea4ea
feat: lake: cache built file hashes
2023-08-30 22:18:33 -04:00
tydeu
c6299eef45
refactor: lake: cleanup Build/Module/Trace code
2023-08-30 22:18:33 -04:00
Scott Morrison
a7efe5b60e
Revert "fix: make sure refine preserves pre-existing natural mvars ( #2435 )" ( #2485 )
...
This reverts commit 0b64c1e330
2023-08-30 08:00:30 +00:00
Scott Morrison
b8084d54e3
doc: update RELEASES.md for rename of getConst? ( #2482 )
2023-08-30 04:44:23 +00:00
