Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merge updated_enabled_cdot. #148

Open
wants to merge 44 commits into
base: main
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
44 commits
Select commit Hold shift + click to select a range
7b034c8
BUG: recompute operator level info in parametrized instantiation
johnyf Dec 7, 2020
3c899a5
BUG: lambdify ENABLED in operators with arguments
johnyf Dec 8, 2020
ab897dc
TST: add tests for `ENABLED` with `INSTANCE`
johnyf Dec 8, 2020
e30f941
TST: correctly detect end of module
johnyf Dec 7, 2020
8a5b74a
BUG: show "VARIABLE" for single variable,
johnyf Dec 8, 2020
c561dbe
ENH: add function `print_modules`
johnyf Dec 7, 2020
aa1f39b
BUG: load modules in `EXTENDS` of submodules
johnyf Dec 7, 2020
09719c8
BUG: correctly shift module units when instantiating
johnyf Dec 8, 2020
4d2129e
REF: add details to error message
johnyf Sep 8, 2020
a4ca6ac
BUG: handle `INSTANCE` statements within `LET`
johnyf Sep 8, 2020
a5dc90a
REF: add details to error message
johnyf Sep 8, 2020
a87906f
BUG: fingerprint `INSTANCE` statements within `LET`
johnyf Sep 8, 2020
93f5186
Merge branch 'let_instance_and_enabled_prm_instance' into merge_let_i…
johnyf Jun 2, 2021
30f1415
liveness proof for EWD840 example
muenchnerkindl Feb 9, 2021
017ebd8
fixed typo in Peterson example
muenchnerkindl Feb 18, 2021
737dd12
DOC: add comments to example and tests
johnyf Nov 12, 2020
f47164b
TST: add TLA+ module `LevelComparisonTest`
johnyf Mar 31, 2021
c7ff69d
TST: add TLA+ module `UnsoundCoalescingThmDecl_test`
johnyf Mar 18, 2021
6b49822
BUG: fingerprint `AutoUSE` results
johnyf Dec 7, 2020
426a200
BUG: correct soundness check for proof levels
johnyf Dec 5, 2020
aec7bbe
DOC: add PlusCal-like algorithm for soundness check
johnyf Dec 5, 2020
987e425
ENH: add proof directives `ENABLEDrules` and `ENABLEDrewrites`
johnyf Dec 5, 2020
70b4eaa
fixup! fpfile changes
johnyf Mar 31, 2021
6a4e5f8
BUG: correct scoping in proof directive `LevelComparison`
johnyf May 25, 2021
23f6f0b
API: print level comparison message only when verbose
johnyf May 26, 2021
c758c25
BUG: correct typo
johnyf Jul 28, 2021
ee56b3d
add labeled arguments in call of expand_enabled_cdot to avoid warning…
quicquid Aug 4, 2022
a963bd3
add example for simple liveness proof, contributed by Andreas Recke
muenchnerkindl Oct 4, 2022
9c27e42
Merge branch 'main' into updated_enabled_cdot
kape1395 Aug 31, 2024
9a6cadd
Print exception backtraces in LSP.
kape1395 Aug 31, 2024
f002d24
Proofs in `examples/EWD840.tla` fixed.
kape1395 Sep 1, 2024
4f4344b
Temporary workaround for making the LSP to work.
kape1395 Sep 1, 2024
cfacd96
Fix proof in `examples/SimpleMutex.tla`.
kape1395 Sep 1, 2024
77ac33f
Fix proof in `examples/SimpleEventually.tla`.
kape1395 Sep 1, 2024
7f63bdd
Properly take the obligation fingerprints in the LSP.
kape1395 Sep 1, 2024
b12dfff
Merge remote-tracking branch 'origin/main' into updated_enabled_cdot
kape1395 Sep 11, 2024
3a04bf6
change magic number for fingerprint files
damiendoligez Nov 12, 2024
609d467
update comment
damiendoligez Nov 19, 2024
e9cca37
Merge pull request #176 from damiendoligez/change-fingerprint-magic
kape1395 Dec 22, 2024
671ac9e
Damien's comments addressed.
kape1395 Dec 22, 2024
c2faf81
Merge remote-tracking branch 'origin/main' into updated_enabled_cdot
kape1395 Dec 22, 2024
9f03ed4
Fixes after the merge.
kape1395 Dec 22, 2024
07d8ce0
Printing to stdout breaks the LSP server, so use stderr.
kape1395 Dec 22, 2024
a9b2e7a
Merge remote-tracking branch 'origin/main' into updated_enabled_cdot
kape1395 Dec 30, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Print exception backtraces in LSP.
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
  • Loading branch information
kape1395 committed Aug 31, 2024
commit 9a6caddd79b5d2ed6e0d0e2871a7e45bda8c1715
3 changes: 2 additions & 1 deletion lsp/lib/server/handlers.ml
Original file line number Diff line number Diff line change
Expand Up @@ -351,7 +351,8 @@ module Make (CB : Callbacks) = struct
with exc ->
let open Jsonrpc.Response.Error in
let exc_str = Printexc.to_string exc in
Eio.traceln "LSP request failed with exception %s" exc_str;
let exc_btr = Printexc.get_backtrace () in
kape1395 marked this conversation as resolved.
Show resolved Hide resolved
Eio.traceln "LSP request failed with exception %s, backtrace:\n%s" exc_str exc_btr;
reply_error req Code.InternalError exc_str state)
| Response resp -> handle_jsonrpc_response resp state
| Batch_call sub_packets ->
Expand Down