Code

Language Server Protocol for TLAPM#93

Code

Merged

kape1395 merged 145 commits intotlaplus:maintlaplus/tlapm:mainfrom kape1395:lspkape1395/tlapm:lspCopy head branch name to clipboardAug 28, 2024

+5,157-96

Commits

Commits on Oct 23, 2023

• Initial experiments with LSP.

  Show description for e09e72d
  kape1395

  committed
  e09e72d

  Copy full SHA for e09e72d

• Empty LSP server works.

  Show description for fc0cd13
  kape1395

  committed
  fc0cd13

  Copy full SHA for fc0cd13

• Some code reorg.

  Show description for 6d06443
  kape1395

  committed
  6d06443

  Copy full SHA for 6d06443

• Use the code formatter.

  Show description for c5e54d4
  kape1395

  committed
  c5e54d4

  Copy full SHA for c5e54d4

• Improving it.

  Show description for e71f936
  kape1395

  committed
  e71f936

  Copy full SHA for e71f936

• CLI added, some refactorings, 2 transports.

  Show description for 705f1cc
  kape1395

  committed
  705f1cc

  Copy full SHA for 705f1cc

• IO Tracing added.

  Show description for 7b6735f
  kape1395

  committed
  7b6735f

  Copy full SHA for 7b6735f

• Some LSP communication works already.

  Show description for 67b1629
  kape1395

  committed
  67b1629

  Copy full SHA for 67b1629

• Option to redirect stderr to a file.

  Show description for 6b90562
  kape1395

  committed
  6b90562

  Copy full SHA for 6b90562

• Use logging to a file rom the ts code.

  Show description for 637f37d
  kape1395

  committed
  637f37d

  Copy full SHA for 637f37d

• Docs store.

  Show description for 687f5a4
  kape1395

  committed
  687f5a4

  Copy full SHA for 687f5a4

• Some experiments on test cases.

  Show description for a6ddb4f
  kape1395

  committed
  a6ddb4f

  Copy full SHA for a6ddb4f

• Handle some LSP packets.

  Show description for ff2d50b
  kape1395

  committed
  ff2d50b

  Copy full SHA for ff2d50b

• Attempt to reuse the original traceln function.

  Show description for cc08f1d
  kape1395

  committed
  cc08f1d

  Copy full SHA for cc08f1d

• Track connection state.

  Show description for fd022ee
  kape1395

  committed
  fd022ee

  Copy full SHA for fd022ee

• Support prover-info cmd.

  Show description for 79eadba
  kape1395

  committed
  79eadba

  Copy full SHA for 79eadba

• Cleanup.

  Show description for d6c7131
  kape1395

  committed
  d6c7131

  Copy full SHA for d6c7131

• Cleanup.

  Show description for bbbc308
  kape1395

  committed
  bbbc308

  Copy full SHA for bbbc308

• Playing with more LSP command types.

  Show description for 31d69e1
  kape1395

  committed
  31d69e1

  Copy full SHA for 31d69e1

• Notes.

  Show description for ac444b2
  kape1395

  committed
  ac444b2

  Copy full SHA for ac444b2

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

  Show description for a54d399
  kape1395

  committed
  a54d399

  Copy full SHA for a54d399

• Some tests.

  Show description for 9bd124e
  kape1395

  committed
  9bd124e

  Copy full SHA for 9bd124e

• Some progress on the tlapm invokation.

  Show description for 413bd17
  kape1395

  committed
  413bd17

  Copy full SHA for 413bd17

• Toolbox parser, support multiline fields.

  Show description for bf54288
  kape1395

  committed
  bf54288

  Copy full SHA for bf54288

• Small code simplifications.

  Show description for 10f8edf
  kape1395

  committed
  10f8edf

  Copy full SHA for 10f8edf

• Some notes.

  Show description for 9316553
  kape1395

  committed
  9316553

  Copy full SHA for 9316553

• Some test cases.

  Show description for 866892d
  kape1395

  committed
  866892d

  Copy full SHA for 866892d

• Support for reading a TLA file from STDIN.

  Show description for eeab4f0
  kape1395

  committed
  eeab4f0

  Copy full SHA for eeab4f0

• Use stream add function instead of stream directly.

  Show description for 0f9da46
  kape1395

  committed
  0f9da46

  Copy full SHA for 0f9da46

• Code reorganized to run on threads.

  Show description for dede4da
  kape1395

  committed
  dede4da

  Copy full SHA for dede4da

• Working on the LSP prove-step command.

  Show description for 7d62986
  kape1395

  committed
  7d62986

  Copy full SHA for 7d62986

• Prover is now invoked.

  Show description for 4db77ad
  kape1395

  committed
  4db77ad

  Copy full SHA for 4db77ad

• TLAPM is now invoked.

  Show description for 8719f7d
  kape1395

  committed
  8719f7d

  Copy full SHA for 8719f7d

• Range translation fixed.

  Show description for d0120d7
  kape1395

  committed
  d0120d7

  Copy full SHA for d0120d7

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

  Show description for 462cad8
  kape1395

  committed
  462cad8

  Copy full SHA for 462cad8

• Structs to maintain obligation state added.

  Show description for 679e556
  kape1395

  committed
  679e556

  Copy full SHA for 679e556

• Notes.

  Show description for 2253767
  kape1395

  committed
  2253767

  Copy full SHA for 2253767

• It starts looking like working.

  Show description for 2b416ed
  kape1395

  committed
  2b416ed

  Copy full SHA for 2b416ed

• Line diff.

  Show description for b7cd138
  kape1395

  committed
  b7cd138

  Copy full SHA for b7cd138

• Docs module reorganized.

  Show description for cd5d78f
  kape1395

  committed
  cd5d78f

  Copy full SHA for cd5d78f

• Diagnostics pull implemented.

  Show description for 32bbf85
  kape1395

  committed
  32bbf85

  Copy full SHA for 32bbf85

• Code formatting.

  Show description for b3bce51
  kape1395

  committed
  b3bce51

  Copy full SHA for b3bce51

• Unify use of diagnostic source.

  Show description for 7ec97db
  kape1395

  committed
  7ec97db

  Copy full SHA for 7ec97db

• Misc fixes.

  Show description for 9ab7d63
  kape1395

  committed
  9ab7d63

  Copy full SHA for 9ab7d63

• Show failed obligation.

  Show description for 2aa1f6f
  kape1395

  committed
  2aa1f6f

  Copy full SHA for 2aa1f6f

• Rename the prove-step command.

  Show description for 989642c
  kape1395

  committed
  989642c

  Copy full SHA for 989642c

• Makefile env setup targets fixed.

  Show description for 46a66f0
  kape1395

  committed
  46a66f0

  Copy full SHA for 46a66f0

• Parser is now invoked.

  Show description for 7b3e2b9
  kape1395

  committed
  7b3e2b9

  Copy full SHA for 7b3e2b9

• Use modules instead of embedded recs.

  Show description for 7870b0a
  kape1395

  committed
  7870b0a

  Copy full SHA for 7870b0a

• Consider theorem ranges when checking a step.

  Show description for cb51893
  kape1395

  committed
  cb51893

  Copy full SHA for cb51893

• A bit of error handling.

  Show description for 8d9d19c
  kape1395

  committed
  8d9d19c

  Copy full SHA for 8d9d19c

• Make build work with older ocaml versions.

  Show description for c58d5e4
  kape1395

  committed
  c58d5e4

  Copy full SHA for c58d5e4

• Experiment: use custom notification to present proof states.

  Show description for 37e8a07
  kape1395

  committed
  37e8a07

  Copy full SHA for 37e8a07

• Notes.

  Show description for 58618d5
  kape1395

  committed
  58618d5

  Copy full SHA for 58618d5

• Proof state is shown somehow.

  Show description for 579804a
  kape1395

  committed
  579804a

  Copy full SHA for 579804a

• Cleanup.

  Show description for 1a72a56
  kape1395

  committed
  1a72a56

  Copy full SHA for 1a72a56

• QED step locus tracking fixed in the parser.

  Show description for 0cc97f9
  kape1395

  committed
  0cc97f9

  Copy full SHA for 0cc97f9

• Code action for "check-proof".

  Show description for 4b6baa8
  kape1395

  committed
  4b6baa8

  Copy full SHA for 4b6baa8

• Use Ocaml 5.1 in the CI build.

  Show description for 2c4b5eb
  kape1395

  committed
  2c4b5eb

  Copy full SHA for 2c4b5eb

• Make CI work with OCaml 5.1.

  Show description for 871a148
  kape1395

  committed
  871a148

  Copy full SHA for 871a148

• Better traceln impl.

  Show description for ca30c58
  kape1395

  committed
  ca30c58

  Copy full SHA for ca30c58

• Use Re2 instead of Str.

  Show description for 5177315
  kape1395

  committed
  5177315

  Copy full SHA for 5177315

• Try improve range calculations.

  Show description for 4425941
  kape1395

  committed
  4425941

  Copy full SHA for 4425941

• Route the obl_num/terminated to the corresponding doc.

  Show description for 83acdf3
  kape1395

  committed
  83acdf3

  Copy full SHA for 83acdf3

• A bit of cleanup.

  Show description for 38403e8
  kape1395

  committed
  38403e8

  Copy full SHA for 38403e8

• Working on the progress presentation and the cancellation.

  Show description for ab6cb52
  kape1395

  committed
  ab6cb52

  Copy full SHA for ab6cb52

• Progress is now shown.

  Show description for 2116c53
  kape1395

  committed
  2116c53

  Copy full SHA for 2116c53

• Cleanup.

  Show description for 7da3374
  kape1395

  committed
  7da3374

  Copy full SHA for 7da3374

• Cancellation support.

  Show description for c72e177
  kape1395

  committed
  c72e177

  Copy full SHA for c72e177

Commits on Nov 11, 2023

• Improve error handling.

  Show description for 7e552c0
  kape1395

  committed
  7e552c0

  Copy full SHA for 7e552c0

• Fixes tlaplus#100.

  Show description for a12ddea
  kape1395

  committed
  a12ddea

  Copy full SHA for a12ddea

Commits on Dec 17, 2023

• Use SigINT to interrupt the TLAPM instead of SigKILL.

  Show description for d0ed4b6
  kape1395

  committed
  d0ed4b6

  Copy full SHA for d0ed4b6

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

  Show description for 07819c6
  kape1395

  committed
  07819c6

  Copy full SHA for 07819c6

Commits on Dec 21, 2023

• Merge remote-tracking branch 'upstream/main' into lsp

  kape1395

  committed
  ccaa8f7

  Copy full SHA for ccaa8f7

Commits on Jan 5, 2024

• Invoke graceful termination on SigINT.

  Show description for 528e0a8
  kape1395

  committed
  528e0a8

  Copy full SHA for 528e0a8

Commits on Jan 7, 2024

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

  Show description for 668db17
  kape1395

  committed
  668db17

  Copy full SHA for 668db17

• Missing lib added, some auto-formatting.

  Show description for 4074c28
  kape1395

  committed
  4074c28

  Copy full SHA for 4074c28

• Make mutex usage compatible with older ocaml versions.

  Show description for 07e89f9
  kape1395

  committed
  07e89f9

  Copy full SHA for 07e89f9

• Broken test fixed.

  Show description for 0cb0251
  kape1395

  committed
  0cb0251

  Copy full SHA for 0cb0251

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

  Show description for f18baaa
  kape1395

  committed
  f18baaa

  Copy full SHA for f18baaa

Commits on Jan 8, 2024

• Adjust the proof state structs for the UI.

  Show description for dd07c14
  kape1395

  committed
  dd07c14

  Copy full SHA for dd07c14

Commits on Jan 12, 2024

• Split tlapm_lsp_docs into multiple files.

  Show description for 0928d79
  kape1395

  committed
  0928d79

  Copy full SHA for 0928d79

• Use HTTPS to download Isabelle.

  Show description for 332a174
  kape1395

  committed
  332a174

  Copy full SHA for 332a174

Commits on Jan 13, 2024

• Take obligation text from the parser.

  Show description for 814e059
  kape1395

  committed
  814e059

  Copy full SHA for 814e059

• Use search path when parsing a document.

  Show description for ec55193
  kape1395

  committed
  ec55193

  Copy full SHA for ec55193

Commits on Jan 14, 2024

• Only show steps from the current file.

  Show description for 9be9d3a
  kape1395

  committed
  9be9d3a

  Copy full SHA for 9be9d3a

Commits on Jan 16, 2024

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

  Show description for 529e001
  kape1395

  committed
  529e001

  Copy full SHA for 529e001

Commits on Jan 21, 2024

• Retain proof state based on fingerprints; attach obligations to steps by range with catch-all.

  Show description for bb88a5e
  kape1395

  committed
  bb88a5e

  Copy full SHA for bb88a5e

Commits on Jan 22, 2024

• Include the BY clauses into the proof step range.

  Show description for b0497da
  kape1395

  committed
  b0497da

  Copy full SHA for b0497da

• Show proof steps for HAVE, TAKE, WITNESS.

  Show description for d26164b
  kape1395

  committed
  d26164b

  Copy full SHA for d26164b

Commits on Jan 23, 2024

• Better error message for unsupported recursive operators.

  Show description for 87788f0
  kape1395

  committed
  87788f0

  Copy full SHA for 87788f0

• Code reorganized into sub-modules.

  Show description for 7db485a
  kape1395

  committed
  7db485a

  Copy full SHA for 7db485a

• Formatter.

  Show description for 8354385
  kape1395

  committed
  8354385

  Copy full SHA for 8354385

• Move range to the main lsp lib.

  Show description for 0311059
  kape1395

  committed
  0311059

  Copy full SHA for 0311059

Commits on Jan 24, 2024

• Prover client code reorganized.

  Show description for 241cfb3
  kape1395

  committed
  241cfb3

  Copy full SHA for 241cfb3

• Reorganize code into sub-modules.

  Show description for 7db97e8
  kape1395

  committed
  7db97e8

  Copy full SHA for 7db97e8

• Progress reorganized.

  Show description for 4ef5e1f
  kape1395

  committed
  4ef5e1f

  Copy full SHA for 4ef5e1f

• Add status to TlapsProofStepDetails.

  Show description for 54e5930
  kape1395

  committed
  54e5930

  Copy full SHA for 54e5930

Commits on Jan 26, 2024

• LSP: omitted and progress fixed.

  Show description for 7d9cb83
  kape1395

  committed
  7d9cb83

  Copy full SHA for 7d9cb83

Commits on Jan 27, 2024

• Misc TODOs addressed.

  Show description for b500bbd
  kape1395

  committed
  b500bbd

  Copy full SHA for b500bbd

• Send updates to the current proof step details.

  Show description for 8bec891
  kape1395

  committed
  8bec891

  Copy full SHA for 8bec891

• Retain decorators after tabs are switched.

  Show description for c00773d
  kape1395

  committed
  c00773d

  Copy full SHA for c00773d

• Set the current proof step via explicit LSP command.

  Show description for 512586b
  kape1395

  committed
  512586b

  Copy full SHA for 512586b

• Send the obligation role with the details.

  Show description for b5aa2a7
  kape1395

  committed
  b5aa2a7

  Copy full SHA for b5aa2a7

Commits on Jan 28, 2024

• Pass obligation status to UI.

  Show description for f006a8f
  kape1395

  committed
  f006a8f

  Copy full SHA for f006a8f

Commits on Jan 30, 2024

• Have to process all the referenced modules.

  Show description for 9289216
  kape1395

  committed
  9289216

  Copy full SHA for 9289216

Commits on Feb 3, 2024

• Exchange module search paths with the LSP client.

  Show description for 14e45b5
  kape1395

  committed
  14e45b5

  Copy full SHA for 14e45b5

• LSP now takes paths from the client.

  Show description for 52d2219
  kape1395

  committed
  52d2219

  Copy full SHA for 52d2219

Commits on Feb 9, 2024

• Add --prefer-stdlib option and use it in the LSP server. This is to solve tlaplus#118.

  Show description for 31ed7d8
  kape1395

  committed
  31ed7d8

  Copy full SHA for 31ed7d8

Commits on Feb 10, 2024

• Global ref to the parser paths eliminated.

  Show description for 1b4437c
  kape1395

  committed
  1b4437c

  Copy full SHA for 1b4437c

• Propagate parser updates to the loaded docs.

  Show description for 777c732
  kape1395

  committed
  777c732

  Copy full SHA for 777c732

Commits on Feb 13, 2024

• Report an understandable error if an operator is applied with a wrong number of arguments.

  Show description for 6231f51
  kape1395

  committed
  6231f51

  Copy full SHA for 6231f51

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

  Show description for 5dc0169
  kape1395

  committed
  5dc0169

  Copy full SHA for 5dc0169

Commits on Feb 17, 2024

• More of error handling in the parser.

  Show description for d3eb73f
  kape1395

  committed
  d3eb73f

  Copy full SHA for d3eb73f

Commits on Feb 26, 2024

• Merge remote-tracking branch 'origin/main' into lsp

  kape1395

  committed
  0a5b5f6

  Copy full SHA for 0a5b5f6

• Merge remote-tracking branch 'upstream/main' into lsp

  kape1395

  committed
  5fa594b

  Copy full SHA for 5fa594b

Commits on May 31, 2024

• Mistype fixed.

  Show description for edfd377
  kape1395

  committed
  edfd377

  Copy full SHA for edfd377

• Update lsp/lib/docs/doc_vsn.ml

  Show description for cee770f
  

  kape1395

  and

  damiendoligez

  committed
  cee770f

  Copy full SHA for cee770f

Commits on Jun 1, 2024

• Remove unused module export.

  Show description for 8dfcaa5
  kape1395

  committed
  8dfcaa5

  Copy full SHA for 8dfcaa5

• Mistype fixed.

  Show description for 70d43c3
  kape1395

  committed
  70d43c3

  Copy full SHA for 70d43c3

• Mistype fixed.

  Show description for 9bb6a52
  kape1395

  committed
  9bb6a52

  Copy full SHA for 9bb6a52

• Mistype fixed.

  Show description for 9d9a559
  kape1395

  committed
  9d9a559

  Copy full SHA for 9d9a559

• Comment refined.

  Show description for 6591218
  kape1395

  committed
  6591218

  Copy full SHA for 6591218

• failwith -> assert false

  Show description for 09c9414
  kape1395

  committed
  09c9414

  Copy full SHA for 09c9414

Commits on Jun 8, 2024

• Use atomic instead of mutex in the signal handler.

  Show description for f653fd7
  

  kape1395

  and

  damiendoligez

  committed
  f653fd7

  Copy full SHA for f653fd7

• Merge remote-tracking branch 'origin/main' into lsp

  Show description for 53cfe83
  kape1395

  committed
  53cfe83

  Copy full SHA for 53cfe83

• Multiple mistypes in comments fixed.

  Show description for 8b8ce33
  

  kape1395

  and

  damiendoligez

  committed
  8b8ce33

  Copy full SHA for 8b8ce33

• Use assert false for impossible cases.

  Show description for 933a762
  

  kape1395

  and

  damiendoligez

  committed
  933a762

  Copy full SHA for 933a762

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

  Show description for f682548
  

  kape1395

  and

  damiendoligez

  committed
  f682548

  Copy full SHA for f682548

• A function simplified.

  Show description for 1865962
  

  kape1395

  and

  damiendoligez

  committed
  1865962

  Copy full SHA for 1865962

• Don't use needless namespaces.

  Show description for 6f7c3ac
  

  kape1395

  and

  damiendoligez

  committed
  6f7c3ac

  Copy full SHA for 6f7c3ac

• Error message improved.

  Show description for 20583b6
  

  kape1395

  and

  damiendoligez

  committed
  20583b6

  Copy full SHA for 20583b6

• Make code more readable.

  Show description for 7491db9
  

  kape1395

  and

  damiendoligez

  committed
  7491db9

  Copy full SHA for 7491db9

• Error message improved.

  Show description for 7865485
  

  kape1395

  and

  damiendoligez

  committed
  7865485

  Copy full SHA for 7865485

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

  Show description for 6b6d9a8
  kape1395

  committed
  6b6d9a8

  Copy full SHA for 6b6d9a8

• Refine the step_loc description.

  Show description for f5fccb3
  kape1395

  committed
  f5fccb3

  Copy full SHA for f5fccb3

Commits on Jun 10, 2024

• Improve comments.

  Show description for c573aba
  kape1395

  committed
  c573aba

  Copy full SHA for c573aba

• Exactly 1 module has to be specified if TLAPM is invoked with the --stdin option.

  Show description for 0ac8eac
  kape1395

  committed
  0ac8eac

  Copy full SHA for 0ac8eac

Commits on Aug 24, 2024

• Update to the new dependency versions.

  Show description for 9e1fbe7
  kape1395

  committed
  9e1fbe7

  Copy full SHA for 9e1fbe7

• Merge remote-tracking branch 'origin/main' into lsp

  Show description for ab37243
  kape1395

  committed
  ab37243

  Copy full SHA for ab37243

Commits on Aug 26, 2024

• Use proper library paths in all cases.

  Show description for 47afb6b
  kape1395

  committed
  47afb6b

  Copy full SHA for 47afb6b

• Improve comments.

  Show description for 0c996a6
  kape1395

  committed
  0c996a6

  Copy full SHA for 0c996a6

• Handle file read errors gracefully.

  Show description for 4837328
  kape1395

  committed
  4837328

  Copy full SHA for 4837328

Commits on Aug 27, 2024

• Toolbox protocol v2 added, fixed the check if an obligation is in the final state.

  Show description for 8138f4b
  kape1395

  committed
  8138f4b

  Copy full SHA for 8138f4b

Commits on Aug 28, 2024

• Cleanup around the pending provers for an obligation.

  Show description for 4d53b9e
  kape1395

  committed
  4d53b9e

  Copy full SHA for 4d53b9e