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

1647 commits

Author SHA1 Message Date
Leonardo de Moura
d0bc4e4245
fix: replace_fn.cpp (#4798) 2024-07-19 21:20:43 -07:00
Leonardo de Moura
3477b0e7f6
fix: for_each_fn.cpp (#4797) 2024-07-20 03:22:56 +00:00
Leonardo de Moura
726e162527
perf: kernel replace with precise cache (#4796) 
Changes:

- We avoid the thread local storage.
- We use a hash map to ensure that cached values are not lost.
- We remove `check_system`. If this becomes an issue in the future we
should precompute the remaining amount of stack space, and use a cheaper
check.
- We add a `Expr.replaceImpl`, and will use it to implement
`Expr.replace` after update-stage0
 2024-07-20 02:00:29 +00:00
Leonardo de Moura
6c33b9c57f
perf: for_each with precise cache (#4794) 
This commit also adds support for `find?` and `findExt?` using kernel
`for_each`.
We need to perform `update-stage0`.
 2024-07-20 00:18:55 +00:00
Joachim Breitner
98ee789990 refactor: InductiveVal.numNested instead of .isNested 
right now, in order to find out how many auxilary datatype are in a
mutual group of inductive with nested data type, one has to jump
through hoops like this:

```
private def numNestedInducts (indName : Name) : MetaM Nat := do
  let .inductInfo indVal ← getConstInfo indName | panic! "{indName} is an inductive"
  let .recInfo recVal ← getConstInfo (mkRecName indName) | panic! "{indName} has a recursor"
  return recVal.numMotives - indVal.all.lengt
```

The `InductiveVal` data structure already has `.isNested : Bool`, so it
seems to be a natural extension to beef that up to `.numNested: Nat`.

This touched kernel code.
 2024-07-08 21:18:50 +02:00
Joachim Breitner
db7a01d126
chore: update comments in kernel/declaration.h (#4683) 
This file has comments that recall the data type definitions in Lean.
Most of them were still using lean3 syntax, and at least one of them was
out of date (one field missing), so I updated them.

I took the liberty to shorten the comments from the original file, or
omit them if they don’t add much over the field names.
 2024-07-08 14:39:43 +00:00
Leonardo de Moura
f5fd962a25
feat: safe exponentiation (#4637) 
Summary:
- Adds configuration option `exponentiation.threshold`
- An expression `b^n` where `b` and `n` are literals is not reduced by
`whnf`, `simp`, and `isDefEq` if `n > exponentiation.threshold`.

Motivation: prevents system from becoming irresponsive and/or crashing
without memory.

TODO: improve support in the kernel. It is using a hard-coded limit for
now.
 2024-07-03 05:12:53 +00:00
Sebastian Ullrich
7f00767b1e
fix: adapt kernel interruption to new cancellation system (#4584) 
Kernel checks were not canceled on edit after #3014
 2024-07-01 14:52:42 +00:00
Leonardo de Moura
7b56eb20a0 feat: prepare for adding new option debug.skipKernelTC 
Remark: I had to comment
```
if debug.skipKernelTC.get opts then
  addDeclWithoutChecking env decl
else
```
because the build was crashing when trying to compile Lake.
Going to perform `update-stage0` and try again.
 2024-06-28 00:55:47 +02:00
Leonardo de Moura
6a040ab068
feat: propagate maxHeartbeats to kernel (#4113) 
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2024-05-09 17:44:19 +00:00
Leonardo de Moura
07c407ab82
feat: collect kernel diagnostic information (#4082) 
We now also track which declarations have been unfolded by the kernel
when using
```lean
set_option diagnostics true
```
 2024-05-06 21:53:16 +00:00
Leonardo de Moura
5c3f6363cc
fix: mismatch between TheoremVal in Lean and C++ (#4035) 2024-04-30 18:10:20 +00:00
Leonardo de Moura
b8b6b219c3
chore: move trace.cpp to kernel (#4014) 
Motivation: trace kernel `is_def_eq`
 2024-04-28 17:24:48 +00:00
Leonardo de Moura
99e8270d2d
fix: proposition fields must be theorems (#4006) 
closes #2575
 2024-04-28 01:59:47 +00:00
Leonardo de Moura
e4daca8d6b
chore: remove dead code at kernel compare (#3966) 2024-04-22 00:54:24 +00:00
Leonardo de Moura
d8d64f1fc0
perf: isDefEq performance issue (#3807) 
Fixes a performance problem found by @hargoniX while working on LeanSAT.
 2024-03-30 02:15:48 +00:00
Leonardo de Moura
84b0919a11 feat: type of theorems must be propositions 2024-03-13 12:37:58 -07:00
Joe Hendrix
1118931516
feat: add bitwise operations to reduceNat? and kernel (#3134) 
This adds bitwise operations to reduceNat? and the kernel. It
incorporates some basic test cases to validate the correct operations
are associated.
 2024-01-11 18:12:45 +00:00
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