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.

Sign up for GitHub

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

Jump to bottom

Language Server Protocol for TLAPM #93

Merged
merged 145 commits into from
Aug 28, 2024
Merged

Language Server Protocol for TLAPM #93

merged 145 commits into from
Aug 28, 2024

Commits on Oct 23, 2023

  1. Initial experiments with LSP. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    e09e72d View commit details
    Browse the repository at this point in the history

  2. Empty LSP server works. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    fc0cd13 View commit details
    Browse the repository at this point in the history

  3. Some code reorg. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    6d06443 View commit details
    Browse the repository at this point in the history

  4. Use the code formatter. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    c5e54d4 View commit details
    Browse the repository at this point in the history

  5. Improving it. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    e71f936 View commit details
    Browse the repository at this point in the history

  6. CLI added, some refactorings, 2 transports. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    705f1cc View commit details
    Browse the repository at this point in the history

  7. IO Tracing added. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    7b6735f View commit details
    Browse the repository at this point in the history

  8. Some LSP communication works already. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    67b1629 View commit details
    Browse the repository at this point in the history

  9. Option to redirect stderr to a file. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    6b90562 View commit details
    Browse the repository at this point in the history

  10. Use logging to a file rom the ts code. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    637f37d View commit details
    Browse the repository at this point in the history

  11. Docs store. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    687f5a4 View commit details
    Browse the repository at this point in the history

  12. Some experiments on test cases. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    a6ddb4f View commit details
    Browse the repository at this point in the history

  13. Handle some LSP packets. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    ff2d50b View commit details
    Browse the repository at this point in the history

  14. Attempt to reuse the original traceln function. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    cc08f1d View commit details
    Browse the repository at this point in the history

  15. Track connection state. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    fd022ee View commit details
    Browse the repository at this point in the history

  16. Support prover-info cmd. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    79eadba View commit details
    Browse the repository at this point in the history

  17. Cleanup. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    d6c7131 View commit details
    Browse the repository at this point in the history

  18. Cleanup. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    bbbc308 View commit details
    Browse the repository at this point in the history

  19. Playing with more LSP command types. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    31d69e1 View commit details
    Browse the repository at this point in the history

  20. Notes. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    ac444b2 View commit details
    Browse the repository at this point in the history

  21. Prove-step now contains the cursor in the doc. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    a54d399 View commit details
    Browse the repository at this point in the history

  22. Some tests. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    9bd124e View commit details
    Browse the repository at this point in the history

  23. Some progress on the tlapm invokation. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    413bd17 View commit details
    Browse the repository at this point in the history

  24. Toolbox parser, support multiline fields. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    bf54288 View commit details
    Browse the repository at this point in the history

  25. Small code simplifications. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    10f8edf View commit details
    Browse the repository at this point in the history

  26. Some notes. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    9316553 View commit details
    Browse the repository at this point in the history

  27. Some test cases. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    866892d View commit details
    Browse the repository at this point in the history

  28. Support for reading a TLA file from STDIN. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    eeab4f0 View commit details
    Browse the repository at this point in the history

  29. Use stream add function instead of stream directly. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    0f9da46 View commit details
    Browse the repository at this point in the history

  30. Code reorganized to run on threads. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    dede4da View commit details
    Browse the repository at this point in the history

  31. Working on the LSP prove-step command. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    7d62986 View commit details
    Browse the repository at this point in the history

  32. Prover is now invoked. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    4db77ad View commit details
    Browse the repository at this point in the history

  33. TLAPM is now invoked. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    8719f7d View commit details
    Browse the repository at this point in the history

  34. Range translation fixed. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    d0120d7 View commit details
    Browse the repository at this point in the history

  35. Obligations are now shown (on proof event only). 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    462cad8 View commit details
    Browse the repository at this point in the history

  36. Structs to maintain obligation state added. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    679e556 View commit details
    Browse the repository at this point in the history

  37. Notes. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    2253767 View commit details
    Browse the repository at this point in the history

  38. It starts looking like working. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    2b416ed View commit details
    Browse the repository at this point in the history

  39. Line diff. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    b7cd138 View commit details
    Browse the repository at this point in the history

  40. Docs module reorganized. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    cd5d78f View commit details
    Browse the repository at this point in the history

  41. Diagnostics pull implemented. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    32bbf85 View commit details
    Browse the repository at this point in the history

  42. Code formatting. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    b3bce51 View commit details
    Browse the repository at this point in the history

  43. Unify use of diagnostic source. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    7ec97db View commit details
    Browse the repository at this point in the history

  44. Misc fixes. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    9ab7d63 View commit details
    Browse the repository at this point in the history

  45. Show failed obligation. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    2aa1f6f View commit details
    Browse the repository at this point in the history

  46. Rename the prove-step command. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    989642c View commit details
    Browse the repository at this point in the history

  47. Makefile env setup targets fixed. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    46a66f0 View commit details
    Browse the repository at this point in the history

  48. Parser is now invoked. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    7b3e2b9 View commit details
    Browse the repository at this point in the history

  49. Use modules instead of embedded recs. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    7870b0a View commit details
    Browse the repository at this point in the history

  50. Consider theorem ranges when checking a step. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    cb51893 View commit details
    Browse the repository at this point in the history

  51. A bit of error handling. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    8d9d19c View commit details
    Browse the repository at this point in the history

  52. Make build work with older ocaml versions. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    c58d5e4 View commit details
    Browse the repository at this point in the history

  53. Experiment: use custom notification to present proof states. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    37e8a07 View commit details
    Browse the repository at this point in the history

  54. Notes. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    58618d5 View commit details
    Browse the repository at this point in the history

  55. Proof state is shown somehow. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    579804a View commit details
    Browse the repository at this point in the history

  56. Cleanup. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    1a72a56 View commit details
    Browse the repository at this point in the history

  57. QED step locus tracking fixed in the parser. 

    Fixes tlaplus#94

Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    0cc97f9 View commit details
    Browse the repository at this point in the history

  58. Code action for "check-proof". 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    4b6baa8 View commit details
    Browse the repository at this point in the history

  59. Use Ocaml 5.1 in the CI build. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    2c4b5eb View commit details
    Browse the repository at this point in the history

  60. Make CI work with OCaml 5.1. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    871a148 View commit details
    Browse the repository at this point in the history

  61. Better traceln impl. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    ca30c58 View commit details
    Browse the repository at this point in the history

  62. Use Re2 instead of Str. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    5177315 View commit details
    Browse the repository at this point in the history

  63. Try improve range calculations. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    4425941 View commit details
    Browse the repository at this point in the history

  64. Route the obl_num/terminated to the corresponding doc. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    83acdf3 View commit details
    Browse the repository at this point in the history

  65. A bit of cleanup. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    38403e8 View commit details
    Browse the repository at this point in the history

  66. Working on the progress presentation and the cancellation. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    ab6cb52 View commit details
    Browse the repository at this point in the history

  67. Progress is now shown. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    2116c53 View commit details
    Browse the repository at this point in the history

  68. Cleanup. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    7da3374 View commit details
    Browse the repository at this point in the history

  69. Cancellation support. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    c72e177 View commit details
    Browse the repository at this point in the history

Commits on Nov 11, 2023

  1. Improve error handling. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Nov 11, 2023
    Configuration menu
    Copy the full SHA
    7e552c0 View commit details
    Browse the repository at this point in the history

  2. Fixes tlaplus#100. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Nov 11, 2023
    Configuration menu
    Copy the full SHA
    a12ddea View commit details
    Browse the repository at this point in the history

Commits on Dec 17, 2023

  1. Use SigINT to interrupt the TLAPM instead of SigKILL. 

    This should close tlaplus#103.

Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Dec 17, 2023
    Configuration menu
    Copy the full SHA
    d0ed4b6 View commit details
    Browse the repository at this point in the history

  2. Buffer proof info updates for some time before sending them to the IDE. 

    This is to decreate load on the IDE, when a lot of proofs are checked fast (e.g. cached). Should close tlaplus#104.

Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Dec 17, 2023
    Configuration menu
    Copy the full SHA
    07819c6 View commit details
    Browse the repository at this point in the history

Commits on Dec 21, 2023

  1. Merge remote-tracking branch 'upstream/main' into lsp

    @kape1395
    kape1395 committed Dec 21, 2023
    Configuration menu
    Copy the full SHA
    ccaa8f7 View commit details
    Browse the repository at this point in the history

Commits on Jan 5, 2024

  1. Invoke graceful termination on SigINT. 

    Closes tlaplus#103
Closes tlaplus/vscode-tlaplus#313

Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 5, 2024
    Configuration menu
    Copy the full SHA
    528e0a8 View commit details
    Browse the repository at this point in the history

Commits on Jan 7, 2024

  1. Initial version of providing the proof state of a step. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 7, 2024
    Configuration menu
    Copy the full SHA
    668db17 View commit details
    Browse the repository at this point in the history

  2. Missing lib added, some auto-formatting. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 7, 2024
    Configuration menu
    Copy the full SHA
    4074c28 View commit details
    Browse the repository at this point in the history

  3. Make mutex usage compatible with older ocaml versions. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 7, 2024
    Configuration menu
    Copy the full SHA
    07e89f9 View commit details
    Browse the repository at this point in the history

  4. Broken test fixed. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 7, 2024
    Configuration menu
    Copy the full SHA
    0cb0251 View commit details
    Browse the repository at this point in the history

  5. Remove test LSP client. It is not relevant anymore. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 7, 2024
    Configuration menu
    Copy the full SHA
    f18baaa View commit details
    Browse the repository at this point in the history

Commits on Jan 8, 2024

  1. Adjust the proof state structs for the UI. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 8, 2024
    Configuration menu
    Copy the full SHA
    dd07c14 View commit details
    Browse the repository at this point in the history

Commits on Jan 12, 2024

  1. Split tlapm_lsp_docs into multiple files. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 12, 2024
    Configuration menu
    Copy the full SHA
    0928d79 View commit details
    Browse the repository at this point in the history

  2. Use HTTPS to download Isabelle. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 12, 2024
    Configuration menu
    Copy the full SHA
    332a174 View commit details
    Browse the repository at this point in the history

Commits on Jan 13, 2024

  1. Take obligation text from the parser. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 13, 2024
    Configuration menu
    Copy the full SHA
    814e059 View commit details
    Browse the repository at this point in the history

  2. Use search path when parsing a document. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 13, 2024
    Configuration menu
    Copy the full SHA
    ec55193 View commit details
    Browse the repository at this point in the history

Commits on Jan 14, 2024

  1. Only show steps from the current file. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 14, 2024
    Configuration menu
    Copy the full SHA
    9be9d3a View commit details
    Browse the repository at this point in the history

Commits on Jan 16, 2024

  1. Proof steps are determined correctly again. Closes tlaplus#114. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 16, 2024
    Configuration menu
    Copy the full SHA
    529e001 View commit details
    Browse the repository at this point in the history

Commits on Jan 21, 2024

  1. Retain proof state based on fingerprints; attach obligations to steps… 

    … by range with catch-all.

Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 21, 2024
    Configuration menu
    Copy the full SHA
    bb88a5e View commit details
    Browse the repository at this point in the history

Commits on Jan 22, 2024

  1. Include the BY clauses into the proof step range. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 22, 2024
    Configuration menu
    Copy the full SHA
    b0497da View commit details
    Browse the repository at this point in the history

  2. Show proof steps for HAVE, TAKE, WITNESS. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 22, 2024
    Configuration menu
    Copy the full SHA
    d26164b View commit details
    Browse the repository at this point in the history

Commits on Jan 23, 2024

  1. Better error message for unsupported recursive operators. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 23, 2024
    Configuration menu
    Copy the full SHA
    87788f0 View commit details
    Browse the repository at this point in the history

  2. Code reorganized into sub-modules. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 23, 2024
    Configuration menu
    Copy the full SHA
    7db485a View commit details
    Browse the repository at this point in the history

  3. Formatter. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 23, 2024
    Configuration menu
    Copy the full SHA
    8354385 View commit details
    Browse the repository at this point in the history

  4. Move range to the main lsp lib. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 23, 2024
    Configuration menu
    Copy the full SHA
    0311059 View commit details
    Browse the repository at this point in the history

Commits on Jan 24, 2024

  1. Prover client code reorganized. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 24, 2024
    Configuration menu
    Copy the full SHA
    241cfb3 View commit details
    Browse the repository at this point in the history

  2. Reorganize code into sub-modules. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 24, 2024
    Configuration menu
    Copy the full SHA
    7db97e8 View commit details
    Browse the repository at this point in the history

  3. Progress reorganized. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 24, 2024
    Configuration menu
    Copy the full SHA
    4ef5e1f View commit details
    Browse the repository at this point in the history

  4. Add status to TlapsProofStepDetails. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 24, 2024
    Configuration menu
    Copy the full SHA
    54e5930 View commit details
    Browse the repository at this point in the history

Commits on Jan 26, 2024

  1. LSP: omitted and progress fixed. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 26, 2024
    Configuration menu
    Copy the full SHA
    7d9cb83 View commit details
    Browse the repository at this point in the history

Commits on Jan 27, 2024

  1. Misc TODOs addressed. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    b500bbd View commit details
    Browse the repository at this point in the history

  2. Send updates to the current proof step details. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    8bec891 View commit details
    Browse the repository at this point in the history

  3. Retain decorators after tabs are switched. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    c00773d View commit details
    Browse the repository at this point in the history

  4. Set the current proof step via explicit LSP command. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    512586b View commit details
    Browse the repository at this point in the history

  5. Send the obligation role with the details. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 27, 2024
    Configuration menu
    Copy the full SHA
    b5aa2a7 View commit details
    Browse the repository at this point in the history

Commits on Jan 28, 2024

  1. Pass obligation status to UI. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 28, 2024
    Configuration menu
    Copy the full SHA
    f006a8f View commit details
    Browse the repository at this point in the history

Commits on Jan 30, 2024

  1. Have to process all the referenced modules. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    9289216 View commit details
    Browse the repository at this point in the history

Commits on Feb 3, 2024

  1. Exchange module search paths with the LSP client. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Feb 3, 2024
    Configuration menu
    Copy the full SHA
    14e45b5 View commit details
    Browse the repository at this point in the history

  2. LSP now takes paths from the client. 

    As a consequence, the TLAPS now accepts JAR paths.
Closes tlaplus#3

Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Feb 3, 2024
    Configuration menu
    Copy the full SHA
    52d2219 View commit details
    Browse the repository at this point in the history

Commits on Feb 9, 2024

  1. Add --prefer-stdlib option and use it in the LSP server. This is to… 

    … solve tlaplus#118.

Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Feb 9, 2024
    Configuration menu
    Copy the full SHA
    31ed7d8 View commit details
    Browse the repository at this point in the history

Commits on Feb 10, 2024

  1. Global ref to the parser paths eliminated. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Feb 10, 2024
    Configuration menu
    Copy the full SHA
    1b4437c View commit details
    Browse the repository at this point in the history

  2. Propagate parser updates to the loaded docs. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Feb 10, 2024
    Configuration menu
    Copy the full SHA
    777c732 View commit details
    Browse the repository at this point in the history

Commits on Feb 13, 2024

  1. Report an understandable error if an operator is applied with a wrong… 

    … number of arguments.

Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Feb 13, 2024
    Configuration menu
    Copy the full SHA
    6231f51 View commit details
    Browse the repository at this point in the history

  2. Register parsing errors so that they can be reported nicely. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Feb 13, 2024
    Configuration menu
    Copy the full SHA
    5dc0169 View commit details
    Browse the repository at this point in the history

Commits on Feb 17, 2024

  1. More of error handling in the parser. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Feb 17, 2024
    Configuration menu
    Copy the full SHA
    d3eb73f View commit details
    Browse the repository at this point in the history

Commits on Feb 26, 2024

  1. Merge remote-tracking branch 'origin/main' into lsp

    @kape1395
    kape1395 committed Feb 26, 2024
    Configuration menu
    Copy the full SHA
    0a5b5f6 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'upstream/main' into lsp

    @kape1395
    kape1395 committed Feb 26, 2024
    Configuration menu
    Copy the full SHA
    5fa594b View commit details
    Browse the repository at this point in the history

Commits on May 31, 2024

  1. Mistype fixed. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed May 31, 2024
    Configuration menu
    Copy the full SHA
    edfd377 View commit details
    Browse the repository at this point in the history

  2. Update lsp/lib/docs/doc_vsn.ml 

    Co-authored-by: Damien Doligez <[email protected]>
Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395 @damiendoligez
    kape1395 and damiendoligez committed May 31, 2024
    Configuration menu
    Copy the full SHA
    cee770f View commit details
    Browse the repository at this point in the history

Commits on Jun 1, 2024

  1. Remove unused module export. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jun 1, 2024
    Configuration menu
    Copy the full SHA
    8dfcaa5 View commit details
    Browse the repository at this point in the history

  2. Mistype fixed. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jun 1, 2024
    Configuration menu
    Copy the full SHA
    70d43c3 View commit details
    Browse the repository at this point in the history

  3. Mistype fixed. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jun 1, 2024
    Configuration menu
    Copy the full SHA
    9bb6a52 View commit details
    Browse the repository at this point in the history

  4. Mistype fixed. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jun 1, 2024
    Configuration menu
    Copy the full SHA
    9d9a559 View commit details
    Browse the repository at this point in the history

  5. Comment refined. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jun 1, 2024
    Configuration menu
    Copy the full SHA
    6591218 View commit details
    Browse the repository at this point in the history

  6. failwith -> assert false 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jun 1, 2024
    Configuration menu
    Copy the full SHA
    09c9414 View commit details
    Browse the repository at this point in the history

Commits on Jun 8, 2024

  1. Use atomic instead of mutex in the signal handler. 

    Co-authored-by: Damien Doligez <[email protected]>
Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395 @damiendoligez
    kape1395 and damiendoligez committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    f653fd7 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/main' into lsp 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    53cfe83 View commit details
    Browse the repository at this point in the history

  3. Multiple mistypes in comments fixed. 

    Co-authored-by: Damien Doligez <[email protected]>
Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395 @damiendoligez
    kape1395 and damiendoligez committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    8b8ce33 View commit details
    Browse the repository at this point in the history

  4. Use assert false for impossible cases. 

    Co-authored-by: Damien Doligez <[email protected]>
Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395 @damiendoligez
    kape1395 and damiendoligez committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    933a762 View commit details
    Browse the repository at this point in the history

  5. Use type nonrec t = t instead of a renamed type. 

    Co-authored-by: Damien Doligez <[email protected]>
Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395 @damiendoligez
    kape1395 and damiendoligez committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    f682548 View commit details
    Browse the repository at this point in the history

  6. A function simplified. 

    Co-authored-by: Damien Doligez <[email protected]>
Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395 @damiendoligez
    kape1395 and damiendoligez committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    1865962 View commit details
    Browse the repository at this point in the history

  7. Don't use needless namespaces. 

    Co-authored-by: Damien Doligez <[email protected]>
Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395 @damiendoligez
    kape1395 and damiendoligez committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    6f7c3ac View commit details
    Browse the repository at this point in the history

  8. Error message improved. 

    Co-authored-by: Damien Doligez <[email protected]>
Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395 @damiendoligez
    kape1395 and damiendoligez committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    20583b6 View commit details
    Browse the repository at this point in the history

  9. Make code more readable. 

    Co-authored-by: Damien Doligez <[email protected]>
Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395 @damiendoligez
    kape1395 and damiendoligez committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    7491db9 View commit details
    Browse the repository at this point in the history

  10. Error message improved. 

    Co-authored-by: Damien Doligez <[email protected]>
Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395 @damiendoligez
    kape1395 and damiendoligez committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    7865485 View commit details
    Browse the repository at this point in the history

  11. Use OCaml 4.14 instead of 4.13. Build a release on 5.1.0. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    6b6d9a8 View commit details
    Browse the repository at this point in the history

  12. Refine the step_loc description. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    f5fccb3 View commit details
    Browse the repository at this point in the history

Commits on Jun 10, 2024

  1. Improve comments. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jun 10, 2024
    Configuration menu
    Copy the full SHA
    c573aba View commit details
    Browse the repository at this point in the history

  2. Exactly 1 module has to be specified if TLAPM is invoked with the `--… 

    …stdin` option.

Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Jun 10, 2024
    Configuration menu
    Copy the full SHA
    0ac8eac View commit details
    Browse the repository at this point in the history

Commits on Aug 24, 2024

  1. Update to the new dependency versions. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Aug 24, 2024
    Configuration menu
    Copy the full SHA
    9e1fbe7 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/main' into lsp 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Aug 24, 2024
    Configuration menu
    Copy the full SHA
    ab37243 View commit details
    Browse the repository at this point in the history

Commits on Aug 26, 2024

  1. Use proper library paths in all cases. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Aug 26, 2024
    Configuration menu
    Copy the full SHA
    47afb6b View commit details
    Browse the repository at this point in the history

  2. Improve comments. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Aug 26, 2024
    Configuration menu
    Copy the full SHA
    0c996a6 View commit details
    Browse the repository at this point in the history

  3. Handle file read errors gracefully. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Aug 26, 2024
    Configuration menu
    Copy the full SHA
    4837328 View commit details
    Browse the repository at this point in the history

Commits on Aug 27, 2024

  1. Toolbox protocol v2 added, fixed the check if an obligation is in the… 

    … final state.

Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Aug 27, 2024
    Configuration menu
    Copy the full SHA
    8138f4b View commit details
    Browse the repository at this point in the history

Commits on Aug 28, 2024

  1. Cleanup around the pending provers for an obligation. 

    Signed-off-by: Karolis Petrauskas <[email protected]>
    @kape1395
    kape1395 committed Aug 28, 2024
    Configuration menu
    Copy the full SHA
    4d53b9e View commit details
    Browse the repository at this point in the history