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

24976 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
3ff7df3675 chore: update stage0 2021-06-06 19:00:10 -07:00
Leonardo de Moura
97a7ef5962 chore: update stage0 2021-06-06 18:57:33 -07: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
Leonardo de Moura
e8a958d8f3 chore: parameter naming convention 2021-06-06 17:09:26 -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
b7ecc1acc3 refactor: Make the non-below version of a premise in the below type for inductive predicates implicit. 
Since it is always fully implied by the below version thereof, it carries no real information and shouldn't be used in pattern matching.
 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
d92e4a7cf1 chore: restore LEANC_EXTRA_FLAGS 
We now pass them to both compilers and linkers. For example, -pthread should be given to both: https://stackoverflow.com/questions/2127797/significance-of-pthread-flag-when-compiling
 2021-06-06 15:34:44 +02:00
Wojciech Nawrocki
c772dc49ef chore: use leanc for all C code 2021-06-06 15:34:44 +02:00
Wojciech Nawrocki
2ef11669e8 chore: reinstate -x c in leanc 2021-06-06 15:34:44 +02:00
Wojciech Nawrocki
4d7ccc7c72 feat: Lean.js can compile itself 2021-06-06 15:34:44 +02:00
Wojciech Nawrocki
91d4011aa8 chore: Emscripten realpath 2021-06-06 15:34:44 +02:00
Wojciech Nawrocki
b7cd68a91e feat: complain more verbosely 2021-06-06 15:34:44 +02:00
Wojciech Nawrocki
7ca87e50ce chore: Emscripten getenv 2021-06-06 15:34:44 +02:00
Wojciech Nawrocki
485f8ea2d0 feat: setup Emscripten file paths 2021-06-06 15:34:44 +02:00
Wojciech Nawrocki
2f97ecb723 chore: restore COPY_LIBS in CMake 2021-06-06 15:34:44 +02:00
Wojciech Nawrocki
7e1faa0be1 chore: fix CMake dependencies 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
407c197236 chore: update stage0 2021-06-06 15:32:58 +02:00
Sebastian Ullrich
67519e226a chore: prepare change 2021-06-06 15:32:58 +02:00
Sebastian Ullrich
7ebe80ad2a chore: update Nix, Nixpkgs, vscode-lean4 2021-06-06 15:00:40 +02:00
Sebastian Ullrich
65efa9603c fix: lean4-mode: show latest file progress data 2021-06-05 17:13:28 +02:00
Sebastian Ullrich
6a76c95bcf feat: lean4-mode: port fringe indicator from lean-mode 2021-06-05 17:13:24 +02:00
Sebastian Ullrich
822f74a35c chore: update stage0 2021-06-05 14:23:00 +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
Sebastian Ullrich
10cf219213 doc: clarify RFC issues 2021-06-04 14:12:59 +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
995136d46b chore: fix test 2021-06-02 10:03:12 -07:00
Leonardo de Moura
55691e2951 chore: update stage0 2021-06-02 10:00:01 -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
e619e7c093 chore: update stage0 2021-06-02 08:31:20 -07:00
Leonardo de Moura
cbab9438c9 chore: Hashable instances for Expr and Level 2021-06-02 08:30:25 -07:00
Leonardo de Moura
d276b47f63 chore: update stage0 2021-06-02 08:08:31 -07:00
Leonardo de Moura
d435b435c5 chore: remove workaround 2021-06-02 08:06:52 -07:00
Leonardo de Moura
d841c2e1d8 chore: remove dead code 2021-06-02 08:04:10 -07:00
Leonardo de Moura
a0eabad8b1 chore: update stage0 2021-06-02 08:01:07 -07:00
Leonardo de Moura
5219593823 chore: use UInt64 to define Name 2021-06-02 08:00:23 -07:00
Leonardo de Moura
30ddaaffe4 chore: update stage0 2021-06-02 07:49:54 -07:00
Leonardo de Moura
5ac2e14173 chore: add Hashable that uses UInt64 2021-06-02 07:47:41 -07:00
Leonardo de Moura
300af47e41 chore: update stage0 2021-06-02 07:25:10 -07:00
Leonardo de Moura
43812444a7 chore: Hashable => HashableUSize 2021-06-02 07:24:26 -07:00