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

16976 commits

Author SHA1 Message Date
Leonardo de Moura
489b28085f feat: simpler and faster RC 2021-07-20 10:42:28 -07:00
Sebastian Ullrich
7e317d23db feat: term info on where declarations 2021-07-19 13:24:59 -07:00
Sebastian Ullrich
b76dd1a8e3 feat: go-to-definition for local variables 2021-07-19 13:24:59 -07:00
Sebastian Ullrich
df57b43b06 fix: go-to-type on parameterized types 2021-07-19 13:24:59 -07:00
Sebastian Ullrich
18becc7d7d fix: plain term goal on binders 2021-07-19 13:24:59 -07:00
Sebastian Ullrich
4a4b4c1ef4 fix: mkAtomFrom: generate synthetic position like other *From functions 
Also consistently use binders as reference position for an elided binder type.
Before, type errors were always given extent 1, the length of the
synthetic `_` token.
 2021-07-19 13:24:59 -07:00
Sebastian Ullrich
904cfd6fcb perf: extract cold path in lean_alloc_small 2021-07-19 13:20:28 -07:00
Sebastian Ullrich
16fbbf98e9 perf: extract cold paths in lean_free_small and mark noinline 2021-07-19 13:20:28 -07:00
Sebastian Ullrich
52810bdfa0 chore: remove dead header 2021-07-19 13:20:28 -07:00
Sebastian Ullrich
8637220927 fix: make precedence mandatory for mixfix commands 
Resolves #577
 2021-07-19 13:18:58 -07:00
Wojciech Nawrocki
caa8f7f7b2 chore: expose Substring.prev/next 2021-07-19 09:55:37 +02:00
Wojciech Nawrocki
f07e49acdb chore: parse names properly 2021-07-19 09:55:37 +02:00
Wojciech Nawrocki
03699cd5ba feat: uniformly split idents 2021-07-19 09:55:37 +02:00
Wojciech Nawrocki
7aca461a35 fix: hovers on elabFieldName fields 2021-07-19 09:55:37 +02:00
Wojciech Nawrocki
b2d712a766 fix: Substring.splitOn 2021-07-19 09:55:37 +02:00
Mario Carneiro
0cf306eb49
chore: fix typo 2021-07-16 10:52:28 +02:00
Wojciech Nawrocki
a8d599a955 fix: typo 2021-07-15 21:57:55 +02:00
Wojciech Nawrocki
eef413cec8 chore: unused binding in FromToJson 2021-07-15 21:57:55 +02:00
Mario Carneiro
c7f5fd6ce4 fix: missing interpolation in trace message 2021-07-15 10:32:37 +02:00
Mario Carneiro
8d616e060b
doc: fix categoryParenthesizer documentation 2021-07-15 09:39:28 +02:00
Daniel Fabian
93a3fd14ad refactor: do not use explicit instance, but use deriving instead. 2021-07-13 09:58:27 -07:00
Daniel Fabian
0d41fd03f7 feat: add xml parser. 
in order to generate the LLVM extern declarations we want to use a generator that spits out XML. Hence adding a small XML parser.
 2021-07-13 09:58:27 -07:00
Wojciech Nawrocki
521ed11330 chore: move parseTagged 
It should live in Lean.Data.Json.FromToJson because many modules import that but not Lean.Elab.Deriving.FromToJson.
 2021-07-12 09:10:29 +02:00
Sebastian Ullrich
f6e1314fa0 chore: LLVM=ON must be used with clang 2021-07-09 11:00:58 +02:00
Sebastian Ullrich
14b9dee84e chore: add missing file 2021-07-09 11:00:58 +02:00
Sebastian Ullrich
b70d018038 feat: include lean.h inline definitions in LLVM module 2021-07-09 11:00:58 +02:00
Sebastian Ullrich
a006558bb3 chore: search for llvm-config in PATH instead of LLVM_TOOLS_BINARY_DIR 
...because it is not there with Nix
 2021-07-09 11:00:58 +02:00
Sebastian Ullrich
5c07c188b4 feat: generate LLVM module of runtime 2021-07-09 11:00:58 +02:00
Sebastian Ullrich
0839ead35e perf: server: avoid redundant publishDiagnostics 
This should reduce server & editor load for the common case where most
command do *not* emit diagnostics
 2021-07-08 12:12:19 +02:00
Wojciech Nawrocki
1ba802418b fix: ToJson for single-field constructors 2021-07-08 09:01:06 +02:00
Sebastian Ullrich
d7dd2fe3ab fix: unbox trivial unparameterized structures as well 2021-07-06 08:19:56 -07:00
Wojciech Nawrocki
6ca8389670 fix: preserve synthetic positions in sanitizer 2021-07-06 09:29:23 +02:00
Wojciech Nawrocki
4ea3d2df2f feat: add missing UInt coercions 2021-07-05 19:42:01 +02:00
Wojciech Nawrocki
fd9e3d8fe6 chore: add completion test and go-to field type 2021-07-05 19:42:01 +02:00
Wojciech Nawrocki
dfcdc57302 feat: go-to for structure fields 2021-07-05 19:42:01 +02:00
Wojciech Nawrocki
24dcdad832 feat: check prefix in option completion 2021-07-05 19:42:01 +02:00
Wojciech Nawrocki
522cbc16d9 fix: typo 2021-07-05 19:42:01 +02:00
Wojciech Nawrocki
c7beb283e9 feat: allow requests to log to stderr 2021-07-05 19:42:01 +02:00
Sebastian Ullrich
99e2a57791 chore: remove unused field Simp.Config.ctorEq 
Resolves #553
 2021-07-05 09:02:20 +02:00
François G. Dorais
1db0bca914 fix: protect Equiv 2021-07-02 10:17:38 -07:00
Leonardo de Moura
5e694d4b69 fix: fixes #536 2021-06-29 18:24:46 -07:00
Leonardo de Moura
f4a7ffd8c8 chore: fix codebase and tests 2021-06-29 17:14:52 -07:00
Leonardo de Moura
90a79a0b06 chore: remove command universes 
Now, `universe` may declare many universes. The goal is to make it
consistent with the `variable` command
 2021-06-29 17:01:07 -07:00
Leonardo de Moura
e9b78585c5 refactor: add BuiltinCommand.lean 2021-06-29 16:52:00 -07:00
Leonardo de Moura
818efe719e fix: fixes #533 2021-06-29 15:20:46 -07:00
Leonardo de Moura
2018dc0959 fix: disable panic messages during initialization 
This is a temporary workaround until we implement #467.
Fixes #534
 2021-06-29 14:48:48 -07:00
Leonardo de Moura
d0358810a7 feat: add lean_set_panic_messages 2021-06-29 14:30:56 -07:00
Sebastian Ullrich
d1f707a6f0 doc: fix typo 
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
 2021-06-29 06:35:45 -07:00
Sebastian Ullrich
9f7af2b77b doc: document a few tactics 2021-06-29 06:35:45 -07:00
Sebastian Ullrich
20fa503803 fix: move elabCommand parts that should happen only once into new function 2021-06-29 06:34:15 -07:00