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

16557 commits

Author SHA1 Message Date
Sebastian Ullrich
32fd82efc2 fix: link lean statically against GMP again 2021-04-14 20:37:07 +02:00
Leonardo de Moura
c1f45ecd48 fix: fixes #394 
The bug was due to the auto-generalization feature.
 2021-04-13 19:14:57 -07:00
Leonardo de Moura
327eb1a96d fix: ensure ill-formed if do-statements do not trigger non termination 2021-04-13 15:51:20 -07:00
Leonardo de Moura
2384826933 chore: add loop prenvention code at do-expander 2021-04-13 15:46:47 -07:00
Leonardo de Moura
1a2a089c28 chore: comment 2021-04-13 10:34:19 -07:00
Leonardo de Moura
adda3a9e02 fix: improve structural recursion 2021-04-13 10:31:43 -07:00
Sebastian Ullrich
435431ca7e feat: hide elaboration errors from partial syntax trees by default 2021-04-13 19:24:35 +02:00
Leonardo de Moura
292bab5a11 fix: loop due to error recovery 2021-04-13 08:12:39 -07:00
Leonardo de Moura
59d7008f24 chore: cleanup 2021-04-13 08:12:14 -07:00
Leonardo de Moura
bf4b9b0ccd fix: use noImplicitLambda% when defining tactic macros such as have, let, etc 
Thus, we don't change the expected type when using them.
 2021-04-12 23:01:47 -07:00
Leonardo de Moura
2f37d7e290 feat: elaborate noImplicitLambda% notation 2021-04-12 22:55:17 -07:00
Leonardo de Moura
635a320455 chore: ignore mdata at intros 2021-04-12 22:38:15 -07:00
Leonardo de Moura
abf78e162c feat: add notation for disabling implicit lambda feature 
This notation will be useful for writing macros where
implicit lambdas are not desired.
 2021-04-12 22:33:23 -07:00
Leonardo de Moura
40a42128be fix: auto completion improvements 2021-04-12 19:22:56 -07:00
Daniel Selsam
d35091da56 feat: parser alias for 'declVal' 2021-04-12 16:59:54 -07:00
Sebastian Ullrich
92810602d0 fix: server: do not stop processing after error (except for header error) 2021-04-12 22:41:10 +02:00
Leonardo de Moura
565ca259b1 fix: issue raised by Andrew 2021-04-12 10:51:44 -07:00
Sebastian Ullrich
1e61b7db89 fix: partial syntax tree panic 
Fixes #391
 2021-04-12 18:33:39 +02:00
Leonardo de Moura
5fc1a86274 chore: indentation 2021-04-11 22:00:21 -07:00
Leonardo de Moura
83b83f51e9 fix: resolveProvider? 
Recent bug fixes exposed a problem here.
The field `resolveProvider?` has a `?`, but is not an `Option`
type. The `ToJson` makes this assumption and uses the auxiliary
function `opt`. The bugs fixed today were masjing this problem.
 2021-04-11 21:45:59 -07:00
Leonardo de Moura
f55561008c fix: fixes #386 2021-04-11 20:57:39 -07:00
Leonardo de Moura
7ae279d04f fix: missing commitWhenSome? at tryPureCoe? 
fixes #389
 2021-04-11 19:28:34 -07:00
Leonardo de Moura
47735d6706 chore: remove dead function 
Moreover, it is incorect to save/restore the metavariable context
without saving/restoring `Term.State` fields contain metavariables
being rolled back.
 2021-04-11 19:17:55 -07:00
Leonardo de Moura
23f49c35fc refactor: MonadBacktrack for TacticM 2021-04-11 19:10:41 -07:00
Leonardo de Moura
484a3a4e7c fix: should only cache inferred type when there are no metavars 2021-04-11 19:10:41 -07:00
Leonardo de Moura
2694e7798a refactor: add MonadBacktrack 
The new class specifies an interface for saving and restoring the
backtrackable part of the state.
This commit also fixes a few issues.

- `commitWhen` at `LevelDefEq` was defining a checkpoint for
  the `isDefEq` methods, and it affects how postponed universe
  constraints are handled. However, the name suggests it is
  similar to `commitWhenSome?`, and consequently it was used
  in other places that had nothing to do with `isDefEq`.
  So, I renamed it, and provided the generic `commitWhen` at the new
  `MonadBacktrack.lean` file.

- We were restoring more state then needed in a few places.
  For example, we were discarding all caches.

- At `SyntheticMVars.lean`, we were using the `Meta.commitWhenSome?`
  method which does not restore the `Term.State`.
 2021-04-11 19:10:41 -07:00
Leonardo de Moura
8917e08251 feat: add tactic macro unhygienic <tactic-seq> 2021-04-10 16:18:40 -07:00
Leonardo de Moura
e56bf66d8d chore: rename option hygienicIntro ==> tactic.hygienic 
It is easier to find.
 2021-04-10 16:09:04 -07:00
Leonardo de Moura
6dbf227cf2 fix: issues #387 part 2 
see #387
 2021-04-10 15:51:07 -07:00
Leonardo de Moura
91cb4aad2a refactor: simplify and document SimpLemma encoding 2021-04-10 15:03:04 -07:00
Leonardo de Moura
4f09390b8e feat: create SimpLemmas.Proof.abst at the simp tactic frontend 2021-04-10 14:17:43 -07:00
Leonardo de Moura
8be9a13679 feat: support for SimpLemma.Proof.abst 2021-04-10 12:46:48 -07:00
Leonardo de Moura
a1205afac2 feat: allow simp lemmas to be AbstractMvarsResult 2021-04-10 11:37:39 -07:00
Leonardo de Moura
3ba9872f33 feat: allow cdot notation at simp 
closes #388
 2021-04-09 19:50:42 -07:00
Leonardo de Moura
57f750ba84 chore: add helper method 2021-04-09 17:53:40 -07:00
Leonardo de Moura
642342d6c1 feat: add Expr.eta 2021-04-09 14:21:21 -07:00
Leonardo de Moura
3318c75bed fix: make sure borrow annotations do not affect auto-completion 2021-04-09 13:47:28 -07:00
Leonardo de Moura
bc8daee635 fix: index out of bounds 2021-04-09 10:09:12 -07:00
Sebastian Ullrich
af588078e0 fix: server: output import errors again 2021-04-09 12:40:38 +02:00
Leonardo de Moura
a1887df4ee feat: include parent structures and aliases in dot notation auto completion 2021-04-08 19:22:31 -07:00
Sebastian Ullrich
cc9577add2 refactor: server: remove SnapshotData 2021-04-08 22:10:27 +02:00
Sebastian Ullrich
dd15c8d5a7 feat: worker: don't abort on import error 
to avoid the "crashed" message
 2021-04-08 22:10:27 +02:00
Sebastian Ullrich
c3d6f781cf refactor: publishDiagnostics 2021-04-08 22:10:27 +02:00
Sebastian Ullrich
bba8184d3b feat: server: treat import errors as fatal 2021-04-08 22:10:27 +02:00
Sebastian Ullrich
a027b34d58 chore: remove dubious server-only option 2021-04-08 22:10:27 +02:00
Leonardo de Moura
a0a4b9faec fix: filter declarations that are not valid dot methods 2021-04-08 11:48:12 -07:00
Sebastian Ullrich
f75ce86f71 fix: server: go to type definition 2021-04-08 18:54:53 +02:00
Sebastian Ullrich
1b1ac393d8 fix: do not try to pretty-print unknown metavariables 
Fixes #380
 2021-04-08 18:16:05 +02:00
Sebastian Ullrich
d75d7aa0d5 fix: server: ignore unknown implementation-dependent notifications 
Fixes #383
 2021-04-08 09:54:36 +02:00
Leonardo de Moura
7de9cfeac8 chore: fix StructInst and add mkGroupNode 2021-04-07 22:46:07 -07:00