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

3612 commits

Author SHA1 Message Date
Sebastian Ullrich
08dbf239a6 chore: server: redundant let 2021-10-15 06:56:02 -07:00
Sebastian Ullrich
674e473c84 feat: server: support LAKE env var 2021-10-15 06:56:02 -07:00
Sebastian Ullrich
6a1897302b chore: server: use exit code to communicate absence of package 2021-10-15 06:56:02 -07:00
Sebastian Ullrich
765ed37409 feat: server: support Lake 2021-10-15 06:56:02 -07:00
Gabriel Ebner
d6ba8e597a feat: add range parameter to getInteractiveDiagnostics 2021-10-11 22:59:47 +02:00
Sebastian Ullrich
e068833e8d fix: register missing simp trace classes 2021-10-11 15:37:56 +02:00
Leonardo de Moura
48a40c4d0a fix: quoteString at EmitC.lean 
Fix issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Incorrect.20escaping.20of.20.5Cr.20.3F/near/257061704
 2021-10-11 06:16:56 -07:00
Leonardo de Moura
002fb7f446 fix: make sure pattern is tried on partial applications 
This commit fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Pattern.20matching.20lambda.20body.20in.20conv/near/256939753
 2021-10-10 15:47:04 -07:00
Leonardo de Moura
04fae18fe4 fix: make sure stop conv pattern stop at first match 2021-10-10 15:47:04 -07:00
Leonardo de Moura
e8bdb66dda fix: make sure we can match pattern inside binders 
This commit fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Pattern.20matching.20lambda.20body.20in.20conv/near/256890867
 2021-10-10 15:47:04 -07:00
Leonardo de Moura
fb27537b8e fix: appUnexpander name resolution 
fixes issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Scoping.20for.20delaborator.3F
 2021-10-09 08:29:26 -07:00
Gabriel Ebner
34eda689a1 fix: use eraseMacroScopes on trace classes 2021-10-08 11:13:19 -07:00
Sebastian Ullrich
0a43a9c466 refactor: use JSON to communicate between server & package manager 2021-10-08 11:28:04 +02:00
Leonardo de Moura
697e0ce2db feat: apply cleanup tactic before applying decreasing tactic 
Alternative design: apply it only before reporting a failure.
 2021-10-06 19:56:57 -07:00
Leonardo de Moura
91d2f6d4fc feat: add cleanup tactic 2021-10-06 19:54:28 -07:00
Leonardo de Moura
c02b4f2675 refactor: move to Meta namespace 2021-10-06 19:05:37 -07:00
Leonardo de Moura
def7641926 feat: add helper methods for checking dependencies 2021-10-06 19:04:02 -07:00
Leonardo de Moura
f10101cd58 fix: preserve user variable names in decreasing goals 2021-10-06 18:45:48 -07:00
Leonardo de Moura
079ad47f02 fix: mixed unary and non-unary functions 2021-10-06 17:33:51 -07:00
Leonardo de Moura
7f660af4c6 feat: add repeat tactic to conv mode 2021-10-06 14:05:44 -07:00
Leonardo de Moura
1f2e92ea04 feat: make sure #check produces some result even when there are pending TC problems 
Lean 3 uses the same approach.

closes #714
 2021-10-06 13:37:06 -07:00
Leonardo de Moura
8ec9fda6c4 fix: improve widening operator used at the ElimDeadBranches abstract interpreter 2021-10-06 12:54:07 -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
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
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
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