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

47 commits

Author SHA1 Message Date
Sebastian Ullrich
8df2b07209 refactor: remove double exception layer in RequestM 2021-11-09 16:58:13 +01:00
Sebastian Ullrich
e92f7f1b4b refactor: server: assume 1 info tree per snapshot 2021-11-04 18:31:36 +01:00
Sebastian Ullrich
fc5082eaef perf: server: reset info trees for each snapshot 2021-11-04 18:31:36 +01:00
Wojciech Nawrocki
0dea880aba doc: diagnostic diff in snapshots 2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
fd016c6065 chore: address some comments 2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
568cc3cf11 refactor: consistent naming of widget modules 2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
f7e9ba76dd perf: cache diagnostics in server 
Reason 1: we were making quadratically many pretty-printer calls since each `publishMessages` would format the entire `MessageLog`.

Reason 2: we want to avoid formatting each diagnostic twice, once as interactive, and once as plain LSP diagnostic.
 2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
c316a8ea69 fix: syntax not updating in header snapshots 2021-08-24 08:57:41 -07:00
Daniel Selsam
6940166db4 chore: rebase and rm rawPos 2021-08-03 09:13:18 +02:00
Daniel Selsam
89364b802b feat: top-down heuristic delaboration 2021-08-03 09:13:18 +02:00
Sebastian Ullrich
20fa503803 fix: move elabCommand parts that should happen only once into new function 2021-06-29 06:34:15 -07:00
Wojciech Nawrocki
4b3987c9cb feat: LSP request handler registration 2021-06-15 22:53:19 +02:00
Sebastian Ullrich
cd5dbc66ce fix: isolate std streams for all commands in server mode 
Fixes #475
 2021-05-19 13:30:54 +02:00
Sebastian Ullrich
e96a21631b refactor: move elaboration error filtering into Elab.Command 
Also make it dependent on presence of `missing` instead of parse error,
which means that messages from complete commands that are immediately followed
by parse errors are not filtered out anymore
 2021-04-17 23:44:57 +02:00
Sebastian Ullrich
435431ca7e feat: hide elaboration errors from partial syntax trees by default 2021-04-13 19:24:35 +02:00
Sebastian Ullrich
cc9577add2 refactor: server: remove SnapshotData 2021-04-08 22:10:27 +02:00
Sebastian Ullrich
a9f96ace3e chore: naming 2021-01-20 16:48:50 +01:00
Sebastian Ullrich
79107a2316 feat: copy & store whole ref range in SourceInfo 2021-01-20 16:48:50 +01:00
Sebastian Ullrich
d7733ba662 feat: use leanpkg print-path for worker initialization 2021-01-19 19:06:01 +01:00
Wojciech Nawrocki
cba3d69e78 feat: enable info trees in server 2021-01-15 13:29:22 -08:00
Sebastian Ullrich
4c3b247dee feat: server: report document symbol hierarchy 2020-12-31 15:00:59 +01:00
mhuisi
563d4f3adc chore: complete rebase and add deriving commands 2020-12-23 20:00:36 +01:00
Marc Huisinga
975b344278 chore: adjust to upstream 2020-12-23 20:00:36 +01:00
Wojciech Nawrocki
c9f88ff89e fix: compare ASTs in the server 
Hopefully this can handle all edge cases.
 2020-12-23 20:00:36 +01:00
Marc Huisinga
8c4becbdd3 chore: superficial refactoring 2020-12-23 20:00:36 +01:00
Wojciech Nawrocki
e0d2af1805 chore: move to new frontend 2020-12-23 20:00:36 +01:00
Wojciech Nawrocki
6ca91ff83c feat: Task-based asynchronous lists 2020-12-23 20:00:36 +01:00
Marc Huisinga
65161d6944 fix: bug where deleting a newline after imports caused incorrect parsing 2020-12-23 20:00:36 +01:00
Sebastian Ullrich
4380d4a9da feat: parser: store options & pass to evalConst 2020-12-16 23:15:58 +01:00
Sebastian Ullrich
21f4257da5 feat: name resolution during parsing 2020-12-03 17:46:13 +01:00
Leonardo de Moura
0869f38de4 chore: update structure, class, inductive 2020-11-27 15:09:30 -08:00
Leonardo de Moura
c305c2691f chore: use := 2020-11-19 07:22:31 -08:00
Leonardo de Moura
16f7bef88f chore: remove old frontend leftovers 2020-10-26 09:08:07 -07:00
Leonardo de Moura
13c2a8ff51 chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
Leonardo de Moura
fa3c32d3b1 chore: remove adaptExcept 2020-10-22 16:56:23 -07:00
Leonardo de Moura
d5612320d7 chore: move to new frontend 2020-10-21 17:12:56 -07:00
Leonardo de Moura
e54a207986 refactor: provide Options to lean_eval_const 
add `ImportM` monad for `addImportedFn`

cc @Kha
 2020-10-19 10:21:38 -07:00
Leonardo de Moura
b72ebe87bd chore: move to new frontend 
@Kha All files at `src/Lean/Elab` are now being compiled with the new
frontend. We can finally claim our elaborator can elaborate itself :)
It is 22% of our code base.
 2020-10-16 12:34:07 -07:00
Leonardo de Moura
ef01053d58 fix: set mainModuleName in the new frontend 2020-10-15 15:30:03 -07:00
Sebastian Ullrich
7083aeea83 chore: adapt to upstream 2020-08-31 06:50:01 -07:00
Wojciech Nawrocki
633acebd0f chore: server style fixes 2020-08-31 06:50:01 -07:00
Wojciech Nawrocki
7a7a14c8b9 chore: no leading commas 2020-08-31 06:50:01 -07:00
Wojciech Nawrocki
f3d640a7cf feat: report parser errors in server 2020-08-31 06:50:01 -07:00
Wojciech Nawrocki
4356017035 chore: copyright 2020-08-31 06:50:01 -07:00
Wojciech Nawrocki
58551721ee chore: namespaces 2020-08-31 06:50:01 -07:00
Wojciech Nawrocki
e1db04d347 feat: more robust snapshot-based recompilation 2020-08-31 06:50:01 -07:00
Wojciech Nawrocki
e137fa780f feat: WIP snapshots 
Allow interactive editing by only recompiling parts of the file below the edit.
 2020-08-31 06:50:01 -07:00