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

2935 commits

Author SHA1 Message Date
Wojciech Nawrocki
4b3987c9cb feat: LSP request handler registration 2021-06-15 22:53:19 +02:00
Wojciech Nawrocki
39931566a0 feat: separate RequestContext in server 2021-06-15 22:53:19 +02:00
Sebastian Ullrich
884aa03584 fix: implement overlooked have syntax 2021-06-15 17:46:16 +02:00
Daniel Selsam
51d26e1172 feat: unexpanders take priority 2021-06-13 09:33:49 +02:00
Daniel Selsam
ded51882a0
feat: pp motives and misc delab fixes 2021-06-13 00:06:27 +02:00
Sebastian Ullrich
4ed66cae3e feat: add --print-prefix, --print-libdir flags 
The names were taken from `llvm-config`
 2021-06-11 17:53:51 -07:00
Sebastian Ullrich
1ebcf76d48 refactor: remove explicitly lifted IO functions and move more things into IO.FS 
Automatic lifting takes care of this, and it wasn't consistently applied anyway
 2021-06-11 17:53:51 -07:00
Leonardo de Moura
a435f3d641 feat: reduce s.1 =?= v to s =?= ⟨v⟩ if structure has a single field 
This feature was suggested by @dselsam at PR #521.
It closes #509
 2021-06-11 11:23:19 -07:00
Gabriel Ebner
94e299a730 fix: instantiate mvars in rewrite tactic 2021-06-11 10:27:05 -07:00
Sebastian Ullrich
cc2f483951 chore: note on previous commit 2021-06-10 18:25:39 +02:00
Sebastian Ullrich
e4bf5977d9 fix: syntax pattern match against multiple identifiers 2021-06-10 18:15:40 +02:00
Gabriel Ebner
47f3cac0c5
fix: server: do not return duplicate response when worker crashes 2021-06-10 09:46:24 +02:00
Gabriel Ebner
f5f9be191b fix: show expected type in term goal 2021-06-07 16:23:22 -07:00
Gabriel Ebner
960cfd9cae feat: store expected type in info tree 2021-06-07 16:23:22 -07:00
Gabriel Ebner
5786f58738 feat: plain term goal request 2021-06-07 16:23:22 -07:00
Sebastian Ullrich
0c3c0ed735 fix: ignore notifications in readResponseAs 2021-06-07 13:21:13 +02:00
Daniel Fabian
63d58c2f64 refactor: use Except instead of Option in the JSON code. 2021-06-07 12:10:10 +02:00
Daniel Fabian
825218cd4a feat: use Except instead of Option in the JSON deriving handlers. 2021-06-07 12:10:10 +02:00
Leonardo de Moura
d8210cd682 feat: mark auxiliary C constants used to store closed terms as static 
This is a workaround to minimize the number of exported symbols in the
Lean executable.
See issues #466 and PR #515
 2021-06-06 18:56:31 -07:00
Daniel Fabian
9200de01ef refactor: fix code review comments. 2021-06-06 06:40:09 -07:00
Daniel Fabian
968ae18f20 fix: deal with params for inductive predicates. 2021-06-06 06:40:09 -07:00
Daniel Fabian
4e53b3bdbf fix: use motive from brecOn in structural recursion for predicates. 2021-06-06 06:40:09 -07:00
Daniel Fabian
4e88fdc99a feat: add getMkMatcherInputInContext. 2021-06-06 06:40:09 -07:00
Daniel Fabian
822c551aa2 test: Add a bunch of test for structural recursion on predicates. 2021-06-06 06:40:09 -07:00
Daniel Fabian
ec6f7d9bd6 feat: Implement structural recursion for inductive predicates. 2021-06-06 06:40:09 -07:00
Wojciech Nawrocki
485f8ea2d0 feat: setup Emscripten file paths 2021-06-06 15:34:44 +02:00
Wojciech Nawrocki
8ada0ba043 feat: initial Emscripten support 2021-06-06 15:34:44 +02:00
Sebastian Ullrich
b82b90a687 feat: KeyedDeclAttribute: expose declaration names 2021-06-06 15:32:58 +02:00
Sebastian Ullrich
67519e226a chore: prepare change 2021-06-06 15:32:58 +02:00
Daniel Fabian
4b7cb058d3 feat: Add support for inductive types to FromJson and ToJson handlers. 2021-06-05 13:53:10 +02:00
Gabriel Ebner
f50647e1c2 doc: describe non-standard requests and notifications 2021-06-05 13:49:28 +02:00
Gabriel Ebner
501c31da4d feat: send $/lean/fileProgress notification 2021-06-05 13:49:28 +02:00
Daniel Fabian
06d1d3ae07 fix: Use UInt64 in deriving handler for Hashable. 2021-06-03 06:38:44 -07:00
Gabriel Ebner
c47fff1b92 fix: cancel queued messages, not pending requests 
Fixes #499.
 2021-06-02 14:46:33 -07:00
Leonardo de Moura
7424f9c8b0 chore: remove HashableUSize 2021-06-02 09:58:46 -07:00
Leonardo de Moura
37da993032 chore: remove HashableUSize instances 2021-06-02 08:48:11 -07:00
Leonardo de Moura
cbab9438c9 chore: Hashable instances for Expr and Level 2021-06-02 08:30:25 -07:00
Leonardo de Moura
d435b435c5 chore: remove workaround 2021-06-02 08:06:52 -07:00
Leonardo de Moura
5219593823 chore: use UInt64 to define Name 2021-06-02 08:00:23 -07:00
Leonardo de Moura
43812444a7 chore: Hashable => HashableUSize 2021-06-02 07:24:26 -07:00
Leonardo de Moura
6a87bba9c0 chore: mixHash => mixUSizeHash 2021-06-02 07:05:42 -07:00
Leonardo de Moura
3499016895 chore: improve error message when compiling code containing axioms or noncomputable definitions 
closes #496
 2021-05-31 20:27:15 -07:00
Leonardo de Moura
764ccc4fb4 chore: add default value for parameter 2021-05-31 18:52:00 -07:00
Leonardo de Moura
7303761569 feat: add modifyTarget 2021-05-31 18:17:07 -07:00
Leonardo de Moura
4062dee864 fix: fixes #498 2021-05-31 15:42:13 -07:00
Sebastian Ullrich
c5957dc069 fix: ignore other leanpkg print-paths output 2021-05-31 17:39:55 +02:00
Sebastian Ullrich
6857076df4 feat: leanpkg build without external dependencies 2021-05-30 17:29:54 +02:00
Sebastian Ullrich
619873c842 feat: make System.FilePath opaque 2021-05-28 14:19:59 +02:00
Sebastian Ullrich
98a4dfc429 fix: module names on case-insensitive platforms 2021-05-28 14:19:59 +02:00
Sebastian Ullrich
4354534fda feat: make FilePath a concrete type 
Resolves #363
 2021-05-28 14:19:59 +02:00