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

1913 commits

Author SHA1 Message Date
Marc Huisinga
ef878bc526 feat: error pending requests in watchdog on termination or crash 2020-12-23 20:00:36 +01:00
Marc Huisinga
c83499a54e feat: add pending requests tracking 2020-12-23 20:00:36 +01:00
Marc Huisinga
1f91f1e194 feat: implement more of the crash-restart behavior 2020-12-23 20:00:36 +01:00
Marc Huisinga
07d5722b67 feat: add explicit process termination procedure, ensure crash handling on writes and accumulate changes of single didChange packet 2020-12-23 20:00:36 +01:00
Marc Huisinga
a8b105e1e9 fix: do not clear diagnostics on empty change packet and add note explaining assumptions about diagnostics 2020-12-23 20:00:36 +01:00
Marc Huisinga
58b66063ee feat: accumulate text changes from same packet in file worker to dispatch their elaboration at once 2020-12-23 20:00:36 +01:00
Marc Huisinga
324235c9fb chore: adjust field naming of WorkerEvent 2020-12-23 20:00:36 +01:00
Marc Huisinga
088c3347cd feat: adjust file worker for new IO features 2020-12-23 20:00:36 +01:00
Marc Huisinga
6f60e3588f feat: file worker termination on header change or file closing 2020-12-23 20:00:36 +01:00
Wojciech Nawrocki
58a04a5478 feat: waitAny event loop in LSP watchdog 2020-12-23 20:00:36 +01:00
Wojciech Nawrocki
bb8f438560 chore: adapt to upstream 2020-12-23 20:00:36 +01:00
Wojciech Nawrocki
cf3d6e8f5e feat: use MonadIO in LSP communication 2020-12-23 20:00:36 +01:00
Wojciech Nawrocki
c3b333b9e7 doc: further comments on server architecture 2020-12-23 20:00:36 +01:00
mhuisi
8decfb6b1d feat: initial multiprocess watchdog arch 2020-12-23 20:00:36 +01:00
Leonardo de Moura
ef51087138 feat: do not log error messages with synthetic sorry's 
Before this commit, only error messages caught at `elabTerm` were
filtered.

cc @Kha
 2020-12-23 10:52:27 -08:00
Leonardo de Moura
f53721e1c9 chore: adapt code to previous change 2020-12-23 08:31:20 -08:00
Leonardo de Moura
e74ba14f4c feat: modify structSimpleBinder parser 
@Kha It felt odd that we can write
```
   map f x := ...
```
in instances, but we had to write
```
   map (f x) := ...
```
when setting the field default value in a class.
 2020-12-23 08:23:14 -08:00
Leonardo de Moura
7720b843bb feat: allow users to use binders when setting default value for parent fields 2020-12-23 08:12:29 -08:00
Leonardo de Moura
7e76446d9d fix: error message 2020-12-23 07:35:12 -08:00
Leonardo de Moura
9c47cfe001 fix: panic message 2020-12-23 07:24:46 -08:00
Leonardo de Moura
78aa3d8e72 chore: use deriving BEq 2020-12-22 18:10:20 -08:00
Leonardo de Moura
df03130927 feat: improve error message 2020-12-22 17:50:26 -08:00
Leonardo de Moura
8c2cb44ac0 fix: error message produced by lean_mk_projections 2020-12-22 17:40:32 -08:00
Leonardo de Moura
9a1116d918 chore: remove <or>, first subsumes it 2020-12-22 14:10:08 -08:00
Leonardo de Moura
832c7412d6 feat: add first tactical 
@Kha It has a few advantages over `<or>` (`<|>`).
- It is not an infix operator.
- It takes tactic sequences instead of tactics as arguments

For example, we can write
```
  first
    | apply h1; assumption
    | exact y; exact h3; assumption
```
or
```
first apply h1; assumption | exact y; exact h3; assumption
```
instead of
```
(apply h1; assumption) <|> (exact y; exact h3; assumption)
```
 2020-12-22 14:10:07 -08:00
Leonardo de Moura
69d83ecb86 chore: make sure term and tactic parsers have disjoint infix operators 2020-12-22 14:10:07 -08:00
Leonardo de Moura
7b813622c6 chore: increase precedence of |>, <|, $ parsers 
@Kha Now, all parsers defined by `Init/Std/Lean` packages have
precedence >= `min` and <= `max`.
The only exception is `<|>` since it is an infix operator sharead with
the tactic DSL.
BTW, the meaning of `f $ a <|> b` changed with this commit.
It was `f (a <|> b)`, and now is `(f a) <|> b`. The problem is that
the precedence of the `$` parser is now greater than the `<|>` parser.

I will try another experiment where I make sure we do not "reuse"
term infix operators in the tactic DSL.
 2020-12-22 14:10:07 -08:00
Leonardo de Moura
cc34733e52 fix: update builtin precedences for |>. and macroDollarArg 2020-12-22 14:10:06 -08:00
Leonardo de Moura
298bdfdcde fix: focus behavior 2020-12-22 14:10:06 -08:00
Leonardo de Moura
289ed6485d feat: eval allGoals 2020-12-22 09:52:54 -08:00
Leonardo de Moura
f638269a71 fix: name resolution at syntax command 
This commit also cleans up `toParserDescr`+`toParserDescrAux`.
 2020-12-22 08:40:00 -08:00
Sebastian Ullrich
93518d4e42 perf: let*-bind syntax match RHSs before duplicating them 2020-12-22 17:25:46 +01:00
Leonardo de Moura
b254aafea0 chore: remove workaround 2020-12-22 07:19:33 -08:00
Leonardo de Moura
7d1e493531 chore: reactivate tactic match and introMatch 2020-12-22 07:15:47 -08:00
Leonardo de Moura
f34bf82e0f chore: move tactic parsers introMatch and match to Lean/Parser/Tactic 2020-12-22 07:11:06 -08:00
Leonardo de Moura
7fa1430a60 chore: add evalMatchTemp 2020-12-22 06:56:58 -08:00
Leonardo de Moura
a05ca020f4 chore: prepare to move tactic match parser back to Lean/Parser/Tactic 2020-12-22 06:52:41 -08:00
Sebastian Ullrich
1c31240ebb feat: token antiquotations in macro 2020-12-22 13:11:04 +01:00
Sebastian Ullrich
07c7638fd7 feat: token source info antiquotations tk%$id 
/cc @leodemoura
 2020-12-22 13:11:04 +01:00
Leonardo de Moura
43255a4af3 feat: local and scoped macros 2020-12-21 17:08:25 -08:00
Leonardo de Moura
0642a62848 chore: prepare to add scoped macro and elab commands 2020-12-21 16:50:29 -08:00
Leonardo de Moura
227b26636c chore: increase default depth to 32 2020-12-21 15:03:27 -08:00
Leonardo de Moura
0083e1996a fix: scoped tokens 
Tokens introduced by scoped (local) parsers should be scoped (local).
 2020-12-21 13:11:09 -08:00
Leonardo de Moura
4fc06bfcca feat: add optional (priority := <prio>) to instance command 2020-12-21 10:02:12 -08:00
Leonardo de Moura
43284cc5fa feat: improve notation for setting parser names and priorities 2020-12-21 09:11:12 -08:00
Sebastian Ullrich
cf73233dd2 refactor: use quotations & implicit token positions from getRef to clean up a bit 2020-12-21 17:32:36 +01:00
Leonardo de Moura
c524bcf2d3 feat: improve universe level pretty printer 2020-12-21 07:34:48 -08:00
Leonardo de Moura
83ae3b7aaa fix: bug introduced when moving to new frontend 2020-12-21 07:34:48 -08:00
Sebastian Ullrich
3e77c7cdef fix: error position 2020-12-21 16:25:01 +01:00
Sebastian Ullrich
756d7643f0 chore: rename syntaxMaxDepth option for consistency and discoverability 
/cc @leodemoura
 2020-12-21 16:25:01 +01:00