max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
31696 commits 1 branch 0 tags 5.3 GiB
Commit graph

31696 commits

This branch
This branch
All branches
Author SHA1 Message Date
tydeu
decf7a042a perf: lake: lazily acquire repo URL/tag in :release 2023-09-25 17:07:27 -04:00
Sebastian Ullrich
2f51d5af49 chore: CI: add backport action 2023-09-25 11:33:14 +02:00
tydeu
2ac782c315 test: lake: add env & dep cfg benchmarks + cleanup 2023-09-22 20:31:48 -04:00
tydeu
16ceb4bf82 perf: lake: no lean --githash when collocated 2023-09-22 16:56:12 -04:00
Sebastian Ullrich
83ecac4fd8 perf: lake: build lakefile environment incrementally 2023-09-22 22:01:07 +02:00
Sebastian Ullrich
c3fd34f933 chore: disable "lake build lean" benchmark for now 2023-09-22 20:05:20 +02:00
Mac Malone
57fb580a71 doc: fix Inundation README typo 
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2023-09-22 20:05:20 +02:00
tydeu
00efb7eaca test: add reconfigure benchmark 2023-09-22 20:05:20 +02:00
tydeu
5b2e3e2b0a test: make compatible with olean caching 2023-09-22 20:05:20 +02:00
tydeu
8dba187910 chore: inundation for configure benchmark 2023-09-22 20:05:20 +02:00
tydeu
7c2ca92661 doc: improve inundation README 2023-09-22 20:05:20 +02:00
tydeu
1d51492139 test: lake: add build Init/Lean/Lake benchmark 2023-09-22 20:05:20 +02:00
tydeu
9a0e57c721 test: add lake benchmarks 2023-09-22 20:05:20 +02:00
tydeu
1354fd9ccd perf: do not detect lean's toolchain 
use `ELAN_TOOLCHAIN` only
 2023-09-21 18:52:52 -04:00
Arthur Adjedj
325fab1c1d
fix: don't try to generate below for nested predicates. (#2390) 
* fix: don't try to generate `below` for nested predicates.

* doc : document test #2389

* doc : document `mkBelow`

* test: extend `2389.lean`

* style: fix comments in `IndPredBelow.lean` and `2389.lean`
 2023-09-21 14:24:37 +10:00
thorimur
e79370a1e6
fix: only return new mvars from refine, elabTermWithHoles, and withCollectingNewGoalsFrom (#2502) 
* fix: `withCollectingNewGoalsFrom`
do not collect old goals

* fix: update occurs check

* test: fix test `run/492.lean`

* docs: add docstring to `elabTermWithHoles`

* test: `refineFiltersOldMVars`

* test: fix `expected.out` name

* test: fix `expected.out` filename and line numbers

* docs: use long ascii dash instead of em dash

Co-authored-by: Scott Morrison <scott@tqft.net>

* docs: fix long line, mention lean4#2502

* docs: a couple more long lines

* test: fix line numbers

---------

Co-authored-by: Scott Morrison <scott@tqft.net>
 2023-09-21 14:23:27 +10:00
tydeu
ec217caf22 feat: lake: add name to manifest 2023-09-20 22:52:39 -04:00
Sebastian Ullrich
dc60150b5a chore: update domain 2023-09-20 15:13:27 -07:00
Sebastian Ullrich
4114ffa273 chore: update stage0 2023-09-20 13:58:13 +02:00
Joachim Breitner
b2d668c340
perf: Use flat ByteArrays in Trie (#2529) 2023-09-20 13:22:37 +02:00
Sebastian Ullrich
de76a5d922
chore: activate stale PR labeler 2023-09-20 09:18:46 +02:00
Patrick Massot
0a59fd96a5
chore: finer-grained ref in getCalcFirstStep (#2563) 
Suggested by @gebner at https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/Random.20calc.20ranges/near/372704972
 2023-09-19 18:58:23 +00:00
Mario Carneiro
f0af71a57b fix: use MoveFileEx for rename on win 2023-09-19 20:24:37 +02:00
Sebastian Ullrich
6bd0a615f1 chore: CI: add workflow_dispatch for stale labeler 2023-09-19 15:29:00 +02:00
Sebastian Ullrich
9038d2e886 chore: disambiguate whnf system category 2023-09-19 05:57:01 -07:00
Sebastian Ullrich
97c4fe3244 chore: CI: label stale PRs 2023-09-19 08:53:23 -04:00
Sebastian Ullrich
0c324a5445 fix: set MACOSX_DEPLOYMENT_TARGET in CI only 2023-09-19 06:11:31 -04:00
Henrik
0d5f9122a1 perf: reduce allocations in unused variable linter 2023-09-18 05:41:37 -04:00
David Renshaw
ba416f2c1c fix: rename parameter of withImportModules to match doc string 2023-09-18 05:40:47 -04:00
Sebastian Ullrich
3e755dc0e1 fix: enforce linebreak between calc steps 2023-09-18 05:39:41 -04:00
thorimur
018020d36f
fix: uninterpolated error message in registerRpcProcedure (#2547) 2023-09-18 11:39:04 +02:00
Scott Morrison
c4bd112a7f
chore: when bumping Mathlib testing branches, bump to latest nightly-testing (#2553) 2023-09-18 02:02:24 +00:00
Scott Morrison
ee3ac9901e
chore: do not generate PR releases from forks (#2550) 2023-09-17 09:28:42 +00:00
Scott Morrison
26de6d3591
chore: begin development cycle for 4.2.0 (#2545) 
* chore: add release notes for #2470 and #2480

* chore: begin development cycle for 4.2.0

* chore: add Lake-related release notes for v4.1.0

---------

Co-authored-by: Mac Malone <tydeu@hatpress.net>
 2023-09-17 14:17:30 +10:00
mhuisi
74b92d9cde chore: remove 'reproduces how often' field from bug template 2023-09-15 14:24:21 +02:00
mhuisi
debd71ec63 chore: make 'impact' a section 2023-09-15 14:24:21 +02:00
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