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

63 commits

Author SHA1 Message Date
Marc Huisinga
382d0474c4 chore: remove dead code and fix some minor styling details 2020-12-23 20:00:36 +01:00
Marc Huisinga
2687a2e582 fix: loss of user input when worker event is received 2020-12-23 20:00:36 +01:00
Marc Huisinga
e066ae1f28 fix: crash handling on cancelRequest, keep looping on forwarding task crash, filter crashed tasks 2020-12-23 20:00:36 +01:00
Wojciech Nawrocki
0e2e2886c8 feat: debugging LSP server via LEAN_SERVER_LOG_DIR 2020-12-23 20:00:36 +01:00
Wojciech Nawrocki
f13b703285 chore: re-add 'runWithInputFile' to server 2020-12-23 20:00:36 +01:00
Sebastian Ullrich
3cdcdac921 feat: infer worker path 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
Wojciech Nawrocki
ca7fee7f0a fix: detect header changes in watchdog 2020-12-23 20:00:36 +01:00
Marc Huisinga
91a8700858 fix: < vs <= bug and add some minor temporary logging 2020-12-23 20:00:36 +01:00
Marc Huisinga
1698c44d2c fix: some silly errors 2020-12-23 20:00:36 +01:00
Marc Huisinga
21474b6d06 feat: dedicated tasks for forwarding 2020-12-23 20:00:36 +01:00
Marc Huisinga
d433fe58af fix: broken pending request filtering in file worker and broken monad instance 2020-12-23 20:00:36 +01:00
Marc Huisinga
e420d101f9 feat: request cancellation 2020-12-23 20:00:36 +01:00
Marc Huisinga
2dfbf81218 feat: shutting down all tasks on termination and file worker termination 2020-12-23 20:00:36 +01:00
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
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
943687ad09 chore: move to new frontend 
@Kha all files at `src/Lean` and `src/Std` have been moved to the new
frontend :)
Next target `src/Init`
 2020-10-21 17:31:25 -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
c54d51b0c9 chore: go back to previous bootstrapping scheme where the stage N+1 stdlib is created using the stage N compiler 2020-09-24 18:57:53 +02: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
70cf20c0ab feat: document Emacs setup 2020-08-31 06:50:01 -07:00
Wojciech Nawrocki
4356017035 chore: copyright 2020-08-31 06:50:01 -07:00
Wojciech Nawrocki
23feb04d60 chore: clean up LSP code style and add more definitions from the spec 2020-08-31 06:50:01 -07:00
Wojciech Nawrocki
098c7af1b6 feat: server tests 2020-08-31 06:50:01 -07:00
Wojciech Nawrocki
86968b5c45 feat: fix UTF-8/16 and add ServerM monad 
Emojis work now 🎉
 2020-08-31 06:50:01 -07:00