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

17769 commits

Author SHA1 Message Date
Leonardo de Moura
106adb09b9 fix: simplify allocator 
Do not move segments between heaps.
We found yet another bug due to this "feature".
The crash is reported here:
https://gist.github.com/semorrison/490496060bbcfa8ea635f3d7be1ac824

@Kha summarized the "root of the evil" as:
using per-heap import lists while segments can be exchanged between heaps doesn't seem compatible.

This is the second bug due to this design decision.
We had fixed one here:
2283ebc5e9/src/runtime/alloc.cpp (L257-L269)

This commit fixes both issues by removing the segment exchange feature.
 2021-10-05 16:58:20 -07:00
Leonardo de Moura
988e43d2b4 fix: WF should reject definitions that do not take any arguments 2021-10-04 13:24:30 -07:00
Wojciech Nawrocki
07f99eba73 fix: use local context from Info node in widgets 2021-10-04 21:09:44 +02:00
Leonardo de Moura
85c49cfeb3 feat: apply termination tactic provided by user 2021-10-03 18:47:52 -07:00
Leonardo de Moura
23740778d4 refactor: termination hints 2021-10-03 18:09:35 -07:00
Leonardo de Moura
d22a42358f feat: add decreasing_tactic notation 2021-10-03 17:16:29 -07:00
Leonardo de Moura
1cdad2be46 fix: missing info trees at let_mvar% elaborator 2021-10-02 20:19:37 -07:00
Leonardo de Moura
53cee4df08 chore: typo 2021-10-02 17:45:08 -07:00
Leonardo de Moura
c908eec8e5 chore: remove temp priority := high 2021-10-02 17:31:55 -07:00
Leonardo de Moura
c24cd877c8 chore: define if-then-else again as a macro 
We can do it using the new auxiliary notation `let_mvar%` and
`wait_if_type_mvar%`.
 2021-10-02 17:30:06 -07:00
Leonardo de Moura
1e44902243 fix: add withFreshMacroScope at expandMacroImpl? 2021-10-02 16:57:25 -07:00
Leonardo de Moura
15347272c7 feat: elaborate wait_* notation 
We can use to define `if-then-else` using macros
 2021-10-02 16:27:22 -07:00
Leonardo de Moura
b510bb305d feat: elaborate let_mvar% 2021-10-02 16:12:50 -07:00
Leonardo de Moura
59d7b00557 feat: add mapping from mvar user name to MVarId 2021-10-02 15:26:44 -07:00
Leonardo de Moura
c6dfecb7aa feat: helper notation for controlling elaboration order 2021-10-02 15:10:27 -07:00
Leonardo de Moura
acd21052c0 chore: remove old notation 2021-10-02 15:06:40 -07:00
Leonardo de Moura
9337498c5b chore: keywords should be snake_case 2021-10-02 14:54:48 -07:00
Leonardo de Moura
b7281e9fe2 fix: instruct pretty printer to add a line break after each calc step 
It should fix https://github.com/leanprover/mathport/issues/26
 2021-10-02 11:38:10 -07:00
Wojciech Nawrocki
f454850c70 fix: actually specify opts-per-pos 2021-10-02 09:55:55 +02:00
Leonardo de Moura
dba358067a chore: remove workaround 2021-09-30 22:37:20 -07:00
Leonardo de Moura
b99f1c698b feat: use if-then-else notation at Do.lean 
Otherwise, the `if` in the `Do` notation will not benefit from the
improved elaborator.
 2021-09-30 22:34:36 -07:00
Leonardo de Moura
eedf5b245f feat: use let_tmp at new if-then-else elaborator 2021-09-30 22:22:14 -07:00
Leonardo de Moura
35d9590b7b chore: rename let_tmp elaborator 2021-09-30 22:20:32 -07:00
Leonardo de Moura
2bc24ff619 chore: let_zeta => let_tmp 2021-09-30 22:19:06 -07:00
Leonardo de Moura
035251d08a feat: elaborate let_zeta 2021-09-30 22:18:47 -07:00
Leonardo de Moura
b83facc738 feat: add let_zeta auxiliary parser 2021-09-30 22:08:11 -07:00
Leonardo de Moura
cc920dd26b feat: new if-then-else elaborator that waits for condition type to be known 2021-09-30 22:07:32 -07:00
Leonardo de Moura
7c0993ae12 chore: add pp annotations to if parser 2021-09-30 20:40:02 -07:00
Leonardo de Moura
88c73f1daa chore: remove old if-then-else parser and elaborator 2021-09-30 20:33:58 -07:00
Leonardo de Moura
7ea23a0f37 chore: reduce priority of old if-then-else parser 2021-09-30 20:31:54 -07:00
Leonardo de Moura
a5502e652c chore: activate builtin if-then-else elaborator 2021-09-30 20:29:49 -07:00
Leonardo de Moura
698760c5eb refactor: add if-then-else builtin parser 2021-09-30 19:33:41 -07:00
Leonardo de Moura
28d81ee456 fix: do not extract closed terms containing constants being defined 
It may produce crashes during initialization.
 2021-09-30 12:46:38 -07:00
Leonardo de Moura
db5df69db4 fix: bounds check 
fixes #704
 2021-09-30 07:55:10 -07:00
Leonardo de Moura
09d0c93589 feat: declare functions in mutual block using auxiliary fuction defined using WF 2021-09-29 11:24:52 -07:00
Leonardo de Moura
608417b946 fix: check number of explicit variables at induction/cases alternatives when @ is not used 
fixes #690
 2021-09-29 07:39:38 -07:00
Leonardo de Moura
3fed9c9df7 feat: reject partial when if constant is not a function 
fixes #697
 2021-09-28 21:07:14 -07:00
Leonardo de Moura
200a38e20c feat: improve letIdLhs parser 
The extra space is only really needed to distinguish an array update (NIY)
```
let x[i] := ...
```
from a declaration taking an instance argument
```
let f [Monad m] := ...
```

closes #696
 2021-09-28 18:10:25 -07:00
Leonardo de Moura
b85d95b7b6 fix: panic in monadic polymorphic code 
fixes #695
 2021-09-28 17:46:19 -07:00
Leonardo de Moura
d0462153a0 fix: bug at smart unfolding procedure 
It fixes an issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Simplifications.20in.20proofs.2Ftype-checking.20not.20happening.3B.20wh.2E.2E.2E
 2021-09-28 10:45:54 -07:00
Sebastian Ullrich
2be3d97cdd chore: leanc: typo & minor modifications 2021-09-28 14:15:58 +02:00
Leonardo de Moura
4c051896df refactor: sizeofMeasure => sizeOfWFRel 
This commit also makes the first argument of `sizeOfWFRel` implicit.
 2021-09-27 19:06:10 -07:00
Leonardo de Moura
bd98e6a586 feat: refine WellFounded.fix functional F over PSigma.casesOn 2021-09-27 19:06:10 -07:00
Leonardo de Moura
d0391d07c2 feat: use PSigma.casesOn instead of projections at packDomain 
Reason: we want to "refine" the `WellFounded.fix` functional `F` over it.
 2021-09-27 19:06:10 -07:00
Leonardo de Moura
8b79176102 feat: refine WellFounded.fix functional F over Sum.casesOn 2021-09-27 19:06:10 -07:00
Leonardo de Moura
f1be1d5bba feat: add simpProj 
Simplifier for kernel projections.
 2021-09-27 19:06:10 -07:00
Leonardo de Moura
c53d892f22 feat: add Expr.projExpr! 2021-09-27 19:06:10 -07:00
Sebastian Ullrich
ae0308fc04 chore: leanc: do not pass linking flags when not linking, again 2021-09-27 17:40:59 +02:00
Leonardo de Moura
108518aad1 feat: use simp at mkDecreasingProof 2021-09-26 16:32:48 -07:00
Leonardo de Moura
d13bdef6e2 feat: add WF.mkFix 2021-09-26 16:01:07 -07:00