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

1629 commits

Author SHA1 Message Date
Sebastian Ullrich
23c68cfc5b fix: remove unguarded check_interrupted call 2023-10-26 08:33:09 +02:00
Sebastian Ullrich
d3bc2ac1a9 fix: switch to C++ interruption whitelist 2023-10-26 08:33:09 +02:00
Sebastian Ullrich
462a583d98 fix: do not throw interrupt exceptions inside pure functions 2023-10-26 08:33:09 +02:00
Sebastian Ullrich
fa3cf4d613 feat: translate interrupted kernel exception 2023-10-26 08:33:09 +02: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
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
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
14c640c15e feat: translate interrupted kernel exception 2023-10-13 09:52:26 +02:00
Mario Carneiro
6bdfde7939 fix: quot reduction bug 2023-10-11 21:25:34 -07:00
Mario Carneiro
b558b5b912 perf: use quick_is_def_eq first 2023-10-11 19:35:16 -07:00
int-y1
ce4ae37c19 chore: fix more typos in comments 2023-10-08 14:37:34 -07:00
Joachim Breitner
06e057758e chore: Remove unused variables from kernel 
when I build lean locally, I get a nice and warning-free build
experience with the exception of these two unused variables. They can
probably go?
 2023-09-27 09:43:07 -07:00
Sebastian Ullrich
9038d2e886 chore: disambiguate whnf system category 2023-09-19 05:57:01 -07:00
Scott Morrison
60b8fdd8d6 feat: use nat_pow in the kernel 2023-07-10 09:01:14 -07:00
Gabriel Ebner
0da281fab4 fix: reject occurrences of inductive type in index 
Fixes #2125
 2023-02-28 12:22:54 -08:00
Leonardo de Moura
decb08858f fix: kernel must ensure that safe functions cannot use partial ones. 
Fix issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Meaning.20of.20.60DefinitionSafety.2Epartial.60
 2023-01-27 12:17:37 -08:00
Gabriel Ebner
34777c9b90 fix: catch missing exceptions in kernel 2023-01-23 09:27:09 -08:00
Sebastian Ullrich
a4abbf07b8 chore: remove remnants of C++ format 2022-11-18 06:11:24 -08:00
Mario Carneiro
a086d217a5 fix: bug in level normalization (soundness bug) 2022-10-26 05:22:26 -07:00
Gabriel Ebner
725aa8b39a refactor: instantiateTypeLevelParams in Lean 2022-10-24 12:23:13 -07:00
Mario Carneiro
dd8bbe9367 fix: catch kernel exceptions in Kernel.{isDefEq, whnf} 
fixes #1756
 2022-10-20 05:38:29 -07:00
Leonardo de Moura
2196a3518e perf: improve lazy_delta_reduction_step heuristic 
It addresses a performance issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/performance.20of.20equality.20with.20projections.2Fmutual/near/288083209
 2022-07-24 11:48:45 -07:00
Gabriel Ebner
c81b10f296 perf: implement Level.update* in Lean 2022-07-19 05:55:13 -07:00
Gabriel Ebner
eda3eae18e perf: implement Expr.update* in Lean 2022-07-19 05:55:13 -07:00
Gabriel Ebner
3176943750 refactor: use computed fields for Level 2022-07-11 14:19:41 -07:00
Leonardo de Moura
451abdf79d fix: Level.update* functions 
see #1291
 2022-07-10 09:16:02 -07:00
Leonardo de Moura
14260f454b feat: improve is_def_eq for projections 
It implements in the kernel the optimization in the previous commit.

This commit addresses the following issue raised on Zulip.
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/unfold.20essentially.20loops/near/288083209
 2022-06-30 17:50:44 -07:00
Leonardo de Moura
69a446c8d1 feat: add field all to DefinitionVal and TheoremVal 
Remark: we need an update stage0, and the field is not being updated
correctly set yet.
 2022-06-23 16:13:26 -07:00
Leonardo de Moura
ca6453a0ab perf: efficient unsigned hash(expr const & e) 2022-03-15 07:15:00 -07:00
Leonardo de Moura
0ef8aaeda0 feat: make sure minor premises in recursors do not include auxiliary type annotations (e.g., autoParam and optParam) 2022-03-10 08:08:36 -08:00
Leonardo de Moura
1afee372f7 refactor: move consume_type_annotations declaration to expr.h 2022-03-10 08:00:39 -08:00
Leonardo de Moura
164f07a5e5 feat: generalize Expr.abstractRange 
It now takes free variables **and** metavariables.
This is the first step to make `mkForallFVars` and `mkLambdaFVars`
more general.
 2022-03-08 18:19:17 -08:00
Leonardo de Moura
f16d8acb29 feat: eager normalization for proofs by reflection 2022-03-01 12:43:55 -08:00
Gabriel Ebner
a7c9d2735f fix: do not apply eta for structures in Prop 
The eta-expansion contains invalid projections, and the eta-rule is
subsumed by proof irrelevance anyhow.
 2022-03-01 09:00:46 -08:00
Gabriel Ebner
3746005f5f fix: reject projection (_ : ∃ x, p).2 
The inferred type of this projection does not even type check, in general.
 2022-03-01 09:00:46 -08:00
Leonardo de Moura
db38bc4043 fix: missing check at infer_proj 
We should not allow `h.1` if `h` is a proposition and the result is
not. The recursor for `h`'s type can only eliminate into `Prop`.
 2022-02-25 07:15:34 -08:00
Leonardo de Moura
f0b502aca6 fix: increase the number of heartbeats at Expr.eqv 
On issue #906, `simp` spends a lot of time checking the cache. This
process is time consuming and doesn't allocate memory. Before this
commit, it would take a long time to get the "maximum number of
heartbeats" error message on the example included in this issue.

Closes #906
 2022-01-26 08:25:33 -08:00
Leonardo de Moura
2d113e83f9 feat: eta struct support for unit-like datatypes 
For example, given `a b : Unit`, we have that `a` and `b` are
definitionally equal by `etaStruct`.

See #777
 2021-11-26 08:36:25 -08:00
Leonardo de Moura
693a96681a doc: fix eta struct comment 2021-11-26 08:36:25 -08:00
Leonardo de Moura
0fc8c1da77 feat: eta for structures at recursors 
see #777
 2021-11-25 11:31:00 -08:00
Leonardo de Moura
50ac21d0a6 refactor: move is_constructor_app to inductive.cpp 2021-11-25 11:31:00 -08:00
Leonardo de Moura
e22bffa94f refactor: move is_structure_like to inductive.cpp 2021-11-25 11:31:00 -08:00
Leonardo de Moura
03e346bc66 chore: simplify to_cnstr_when_K 2021-11-25 11:31:00 -08:00
Leonardo de Moura
a8f4146070 feat: support eta struct recursively 
Addresses issues raised by @gebner at #777
 2021-11-23 17:38:48 -08:00
Leonardo de Moura
d685c545b4 feat: eta for structures 2021-11-23 06:21:25 -08:00
Leonardo de Moura
80a73dd903 feat: basic support for definitions at inductive declarations 2021-10-25 12:44:35 -07:00
Sebastian Ullrich
b13d3e6ca5 fix: dllexport functions not already annotated in header 2021-09-20 18:41:46 +02:00
Leonardo de Moura
c8406a301d chore: reduce src/include/lean 2021-09-07 08:24:54 -07:00
Leonardo de Moura
cf49e6fe8f fix: binder name 
Binder names are relevant for the `induction` tactic.
 2021-08-26 11:11:37 -07:00