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

31791 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
a7323c9805 feat: use forall_prop_domain_congr in simp tactic 
closes #1926
 2023-10-23 06:19:19 -07:00
Leonardo de Moura
50d0aced7f feat: add auxiliary lemma for simp 2023-10-23 06:19:19 -07:00
Leonardo de Moura
0bd15be1a1 chore: fix tests output 2023-10-22 06:48:22 -07:00
Leonardo de Moura
370476cc14 fix: bug at substCore 2023-10-22 06:48:22 -07:00
Leonardo de Moura
9a7565d66c perf: closes #2552 2023-10-22 06:48:22 -07:00
Leonardo de Moura
52f1000955 chore: update doc, add support for modn 2023-10-20 19:07:48 -07:00
Leonardo de Moura
9d02e0ee6f chore: remove unnecessary % operations at Fin.mod and Fin.div 
We now have the missing proofs `Nat.mod_le` and `Nat.div_le_self` in
core.
See:
https://github.com/leanprover/std4/pull/286#discussion_r1359807875
 2023-10-20 19:07:48 -07:00
thorimur
1facbde113 test: ensure dsimp can use rfl thm constants 2023-10-20 19:06:40 -07:00
thorimur
b5e95bf632 fix: allow constants to be marked for dsimp 2023-10-20 19:06:40 -07:00
tydeu
6c20673737 refactor: change postUpdate? config to a decl 2023-10-20 21:38:31 -04:00
github-actions[bot]
b52317537c doc: update changelog 2023-10-20 18:51:37 +00:00
tydeu
6e98453189 chore: lake: test auto-manifest & update cleaning 2023-10-20 14:51:10 -04:00
tydeu
e435a45af7 feat: lake: create manifest on load if missing 2023-10-20 14:51:10 -04:00
Leonardo de Moura
419100d42b feat: add Simp.Config.ground for simplifying nested ground terms 
This is an experimental new feature. We need more bells and whistles,
and `cbv` tactic for improving its performance.
 2023-10-19 13:59:17 -07:00
tydeu
67b5cd9c0e feat: lake: run_io to execute IO at term elab time 2023-10-19 13:27:35 -04:00
tydeu
ca6d1fd47a chore: lake: simplify config decl syntax 
* deprecate `:=` syntax in config decls
* standardize field syntax across `where` and `{...}`
 2023-10-19 13:25:07 -04:00
Scott Morrison
fb0d0245db
Revert "Cancel outstanding tasks on document edit in the language server" (#2703) 
* Revert "perf: inline `checkInterrupted`"

This reverts commit 6494af4513.

* Revert "fix: switch to C++ interruption whitelist"

This reverts commit 5aae74199b.

* Revert "fix: do not throw interrupt exceptions inside pure functions"

This reverts commit c0e3b9568e.

* Revert "feat: cancel tasks on document edit"

This reverts commit a2e2481c51.

* Revert "feat: translate `interrupted` kernel exception"

This reverts commit 14c640c15e.

* Revert "feat: check task cancellation in elaborator"

This reverts commit 2070df2328.

* Revert "feat: move `check_interrupted` from unused thread class to `Task` cancellation"

This reverts commit bf48a18cf9.
 2023-10-17 00:59:11 +00:00
SADIK KUZU
e0802d2dea
fix: typos in specialize.cpp (#2702) 2023-10-17 00:58:10 +00:00
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
894c3abb37 chore: lake: ignore manifest in examples/scripts 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
Mario Carneiro
e0cba05167
refactor: env extensions can only modify .extensions (#2661) 2023-10-16 14:22:09 +11:00
Scott Morrison
2f9c964753
chore: update RELEASES.md to reflect v4.2.0-rc2 (#2692) 2023-10-16 01:19:12 +00:00
Mario Carneiro
c0b021e196 fix: pp projection indices starting at 1 2023-10-15 14:25:00 -07:00
Scott Morrison
3e79ddda27
chore: add items to RELEASES.md (#2687) 2023-10-15 02:51:58 +00:00
Scott Morrison
1e74c6a348
feat: use nat_gcd in the kernel (#2533) 
* feat: use nat_gcd in the kernel

---------

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2023-10-15 13:49:41 +11:00
Scott Morrison
66ab016723
chore: simp tracing reports ← (#2621) 
* chore: simp tracing reports ←

---------

Co-authored-by: Mario Carneiro <di.gama@gmail.com>
 2023-10-15 12:12:10 +11:00
github-actions[bot]
6df09d16e5 doc: update changelog 2023-10-14 17:20:54 +00:00
Leonardo de Moura
b8af36fba0 chore: update comments at src/Lean/Meta/Basic.lean 
Co-authored-by: Timo <timorcb@gmail.com>
 2023-10-14 10:20:29 -07:00
Leonardo de Moura
29198371d9 chore: update comments at src/Lean/Meta/ExprDefEq.lean 
Co-authored-by: Timo <timorcb@gmail.com>
 2023-10-14 10:20:29 -07:00
Leonardo de Moura
3bc18797b0 fix: ensure transient cache results for different transparency modes don't mix up 2023-10-14 10:20:29 -07:00
Sebastian Ullrich
6d0a3287e0 fix: cache typos 2023-10-14 10:20:29 -07:00
Leonardo de Moura
e3b08060d0 fix: chore add workaround for corrupted cache 2023-10-14 10:20:29 -07:00
Leonardo de Moura
2253b788b4 perf: fine grain isDefEq cache for terms not containing metavariables 2023-10-14 10:20:29 -07:00
Arthur Adjedj
ff20a14c69
fix : make mk_no_confusion_type handle delta-reduction when generating telescope (#2501) 
* fix : make `mk_no_confusion_type` handle delta-reduction when checking the inductive type.

* tests: extend `2500.lean`
 2023-10-14 17:18:37 +11:00
mhuisi
d0ae87d13f chore: improve error 2023-10-13 16:42:19 +02:00
mhuisi
b5348786a6 fix: pre-dependency-build-mode compatibility 2023-10-13 16:42:19 +02:00
mhuisi
253a5b931d fix: correct handling of FileWorker restarts 2023-10-13 16:42:19 +02:00
mhuisi
9945fa04d6 feat: FileWorker handling of --no-build 2023-10-13 16:42:19 +02:00
Sebastian Ullrich
4e1d95ce58 feat: pass along extra print-paths flags and handle no-build Lake error in server 2023-10-13 16:42:19 +02:00
tydeu
f3de5eb1e8 feat: lake: --no-build to exit before a build 2023-10-13 14:42:58 +02:00
github-actions[bot]
9f63a9f288 doc: update changelog 2023-10-13 07:57:12 +00:00
Sebastian Ullrich
6494af4513 perf: inline checkInterrupted 
Amazingly, the extra result allocation seems to have triggered a mathlib
heartbeat timeout
 2023-10-13 09:52:26 +02:00
Sebastian Ullrich
5aae74199b fix: switch to C++ interruption whitelist 2023-10-13 09:52:26 +02:00
Sebastian Ullrich
c0e3b9568e fix: do not throw interrupt exceptions inside pure functions 2023-10-13 09:52:26 +02:00
Sebastian Ullrich
a2e2481c51 feat: cancel tasks on document edit 2023-10-13 09:52:26 +02:00
Sebastian Ullrich
14c640c15e feat: translate interrupted kernel exception 2023-10-13 09:52:26 +02:00
Sebastian Ullrich
2070df2328 feat: check task cancellation in elaborator 2023-10-13 09:52:26 +02:00