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

199 commits

Author SHA1 Message Date
Sebastian Ullrich
d6eab393f4
chore: fix benchmark 2024-06-20 18:18:41 +02:00
Marc Huisinga
3119fd0240
fix: make watchdog more resilient against badly behaving clients (#4443) 
This PR addresses some non-critical but annoying issues that sometimes
cause the language server to report an error:
- When using global search and replace in VS Code, the language client
sends `textDocument/didChange` notifications for documents that it never
told the server to open first. Instead of emitting an error and crashing
the language server when this occurs, we now instead ignore the
notification. Fixes #4435.
- When terminating the language server, VS Code sometimes still sends
request to the language server even after emitting a `shutdown` request.
The LSP spec explicitly forbids this, but instead of emitting an error
when this occurs, we now error requests and ignore all other messages
until receiving the final `exit` notification. Reported on Zulip several
times over the years but never materialized as an issue, e.g.
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Got.20.60shutdown.60.20request.2C.20expected.20an.20.60exit.60.20notification/near/441914289.
- Some language clients attempt to reply to the file watcher
registration request before completing the LSP initialization dance. To
fix this, we now only send this request after the initialization dance
has completed. Fixes #3904.

---------

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2024-06-13 13:48:36 +00:00
Joachim Breitner
4f50544242
chore: Nat.repr microbenchmark (#3888) 2024-04-17 18:10:32 +00:00
Sebastian Ullrich
6712913bfe chore: update cross-bench setup 2024-04-15 10:59:07 +02:00
David Thrane Christiansen
966fa800f8
chore: remove the coercion from String to Name (#3589) 
This coercion caused difficult-to-diagnose bugs sometimes. Because there
are some situations where converting a string to a name should be done
by parsing the string, and others where it should not, an explicit
choice seems better here.

---------

Co-authored-by: Mac Malone <tydeu@hatpress.net>
 2024-03-21 23:46:03 +00:00
Marc Huisinga
093e1cf22a
test: add language server startup benchmark (#3558) 
Benchmark to catch future regressions as the one fixed in #3552.
 2024-03-04 09:01:51 +00:00
Sebastian Ullrich
c9aea32d3e
chore: speedcenter: count max symbols in shared libraries (#3418) 2024-02-20 19:25:24 +00:00
Scott Morrison
88deb34ddb
chore: upstream omega (#3367) 
Co-authored-by: Joe Hendrix <joe@lean-fro.org>
 2024-02-19 00:19:55 +00:00
Joe Hendrix
8f010a6115
fix: liasolver benchmark bug introduced by #3364 (#3372) 
This fixes a rounded division/mod bug introduced by the change in
semantics from Int.div to Int.mod in #3364.
 2024-02-16 23:39:26 +00:00
Sebastian Ullrich
8bc1a9c4ba
chore: actually include full build in benchmark (#3158) 
I must have reverted too much while testing #3104
 2024-01-10 14:33:27 +00:00
Sebastian Ullrich
caf7a21c6f
chore: include full build in stdlib benchmark (#3104) 2023-12-23 16:27:07 +00:00
Sebastian Ullrich
767139b235
chore: use all cores in stdlib benchmark 2023-12-21 10:37:18 +01:00
Sebastian Ullrich
b278172b7c chore: add import Lean benchmark 2023-11-07 18:46:28 +01:00
Sebastian Ullrich
00e981edcd perf: do not inhibit caching of default-level match reduction 2023-10-08 17:24:20 -07:00
int-y1
ce4ae37c19 chore: fix more typos in comments 2023-10-08 14:37:34 -07:00
tydeu
2ac782c315 test: lake: add env & dep cfg benchmarks + cleanup 2023-09-22 20:31:48 -04:00
Sebastian Ullrich
c3fd34f933 chore: disable "lake build lean" benchmark for now 2023-09-22 20:05:20 +02:00
Mac Malone
57fb580a71 doc: fix Inundation README typo 
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2023-09-22 20:05:20 +02:00
tydeu
00efb7eaca test: add reconfigure benchmark 2023-09-22 20:05:20 +02:00
tydeu
5b2e3e2b0a test: make compatible with olean caching 2023-09-22 20:05:20 +02:00
tydeu
8dba187910 chore: inundation for configure benchmark 2023-09-22 20:05:20 +02:00
tydeu
7c2ca92661 doc: improve inundation README 2023-09-22 20:05:20 +02:00
tydeu
1d51492139 test: lake: add build Init/Lean/Lake benchmark 2023-09-22 20:05:20 +02:00
tydeu
9a0e57c721 test: add lake benchmarks 2023-09-22 20:05:20 +02:00
tydeu
926663505e chore: split up & simplify importModules 2023-08-31 15:37:33 -04:00
Sebastian Ullrich
bb738796ae test: update parser benchmark, add to speedcenter suite 2023-08-08 18:40:19 +02:00
Sebastian Ullrich
d62fca4e9c chore: safer bench script 2023-07-19 08:31:39 +02:00
Leonardo de Moura
fd0549feb5 chore: improve test 2023-07-11 19:19:42 -07:00
Leonardo de Moura
6d857a93b5 perf: pointer set for traversing DAGs 2023-07-11 19:19:42 -07:00
Connor Baker
667d54640d
chore: Nix: use strings instead of URL literals (#2172) 2023-03-28 10:10:24 +02:00
Sebastian Ullrich
b81cff87bc chore: update temci 2023-03-24 11:34:21 +01:00
Sebastian Ullrich
83c1a1ab77 chore: bench: update temci 2023-03-16 16:39:50 +01:00
Sebastian Ullrich
4cc6057f4a chore: ensure consistent (Unix) encoding for source files 2023-03-10 16:27:56 +01:00
Sebastian Ullrich
3146aa477d fix: accumulate_profile: accept category names containing digits (e.g. hygiened decl names) 2023-02-11 17:41:07 +01:00
Sebastian Ullrich
1f41b91206 test: update Lean variant benchmarks 2023-01-26 13:33:28 +01:00
Sebastian Ullrich
12356b739b test: add rbmap_2 benchmark 2023-01-26 13:32:42 +01:00
Sebastian Ullrich
cbdd76f6b6 test: retire .perf benchmarks, cache misses are not very enlightening 2023-01-19 14:44:20 +01:00
Sebastian Ullrich
d0ca604d89 test: update mlton 2023-01-19 14:44:20 +01:00
Sebastian Ullrich
899b673531 test: add binarytrees.st benchmark 2023-01-19 14:44:20 +01:00
Sebastian Ullrich
83450d4bd9 test: clean up binarytrees.lean 2023-01-19 14:44:20 +01:00
Sebastian Ullrich
46f467db66 test: add single-threaded SML binarytrees 2023-01-19 14:44:20 +01:00
Sebastian Ullrich
78bc2fd92b chore: more benchmarking setup 2023-01-17 13:28:05 +01:00
Sebastian Ullrich
9b1f5c4df4 test: use OCaml 5 multicore binarytrees implementation 2023-01-12 18:28:41 +01:00
Sebastian Ullrich
f726891baf test: update benchmark flake 2023-01-12 18:28:41 +01:00
Siddharth
b6eb780144
feat: LLVM backend (#1837) 2022-12-30 12:45:30 +01:00
Sebastian Ullrich
6b8fa76265 test: benchmark workspace symbols search 2022-10-13 21:41:58 +02:00
Sebastian Ullrich
18a4b277fc test: more fair qsort.ml benchmark 2022-10-12 20:22:55 +02:00
Sebastian Ullrich
5b7e6661f9 chore: more RBMap cleanup 2022-10-06 17:26:43 -07:00
Sebastian Ullrich
6f4cea6dba feat: add rbmap_fbip benchmark 2022-10-06 17:26:43 -07:00
Mario Carneiro
85119ba9d1 chore: move Std.* data structures to Lean.* 2022-09-26 05:46:04 -07:00