Clicking on a module name on the EXTENDS line should open the module

[lemmy]

If one clicks on a module name on the EXTENDS line in the toolbox, an editor for that module is opened (including standard modules).

[peterzeller]

Hello, potential first-time contributor here, coming from Twitter. I would like to work on this issue.

I had a short look at the code now and I would start with an approach like this:

• Add test in tests/suite/declarations/tlaDeclarations.test.ts
• Extend src/declarations/tlaDeclarations.ts
  • test whether word at selected position appears is part of a module list after EXTENDS
  • open an editor with the corresponding module file. I need to check the lookup rules of TLA, but I guess it is somewhat like this:
    • if there is a file with the correct module name in the same directory, use this as the link
    • otherwise, if there is a standard library module, extract it to some temporary directory to get a normal file url (or check if there is some kind of virtual file support in vscode)
      • I have to check how I can find standard library modules, maybe tla tools can be invoked to get them, or I need to extract them from the tla+ jar. Would be thankful for a hint on where to look.

Does this sound like a good plan?

An alternative approach I could think of would be to extend the Java code of TLA+ to expose the functionality used in the Eclipse editor. If I see it correctly, the Eclipse editor uses the syntax tree to resolve links (TLAHyperlinkDetector.java), which seems to be more robust than doing some text searches.

[lemmy]

@peterzeller Thanks for volunteering! :-)

Agreed! Ideally, this is implemented as a lookup into SANY's AST similar to how it is done in TLAHyperlinkDetector.java. That way, the Eclipse and VSCode editors would be guaranteed to behave the same. Unfortunately, I don't see where the VSCode extension has access to the parse tree. We could push what is implemented in TLAHyperlinkDetector.java into SANY, though, and expose it on the command line. Most of this is already available in tla2sany.explorer.Explorer.main(String[]) (launch through tla2sany.drivers.SANY). Specifically, Explorer gives you access to SANY's module table:

****** SANY2 Version 2.2 created 08 July 2020

Parsing file /Users/markus/tlaplus/git/examples.tlapl.us/specifications/ewd998/EWD998.tla
Parsing file /Users/markus/tlaplus/git/tlaplus/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/Integers.tla
Parsing file /Users/markus/tlaplus/git/tlaplus/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/FiniteSets.tla
Parsing file /Users/markus/tlaplus/git/examples.tlapl.us/specifications/ewd998/Utils.tla
Parsing file /Users/markus/tlaplus/git/tlaplus/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/Naturals.tla
Parsing file /Users/markus/tlaplus/git/tlaplus/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/Sequences.tla
Parsing file /Users/markus/tlaplus/git/tlaplus/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/TLC.tla
Parsing file /private/var/folders/rn/dpqg4cgn7lg6k4_qwcx2jhvr0000gn/T/tlc-8038721644179407749/Functions.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Functions.tla)
Parsing file /private/var/folders/rn/dpqg4cgn7lg6k4_qwcx2jhvr0000gn/T/tlc-8038721644179407749/SequencesExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/SequencesExt.tla)
Parsing file /Users/markus/tlaplus/git/examples.tlapl.us/specifications/ewd998/AsyncTerminationDetection.tla
Parsing file /private/var/folders/rn/dpqg4cgn7lg6k4_qwcx2jhvr0000gn/T/tlc-8038721644179407749/Folds.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/Folds.tla)
Parsing file /private/var/folders/rn/dpqg4cgn7lg6k4_qwcx2jhvr0000gn/T/tlc-8038721644179407749/FiniteSetsExt.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/CommunityModules-deps.jar!/FiniteSetsExt.tla)
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module Folds
Semantic processing of module Functions
Semantic processing of module FiniteSetsExt
Semantic processing of module SequencesExt
Semantic processing of module Utils
Semantic processing of module AsyncTerminationDetection
Semantic processing of module EWD998


*** TLA+ semantic graph exploration tool v 1.0 (DRJ)

>>cst
*** Concrete Syntax Tree for Module 401
N_Module	  #heirs: 4	  kind:   382
| N_BeginModule	  #heirs: 3	  kind:   333
| | ---------------------------- MODULE	  #heirs: 0	  kind:   3
| | FiniteSets	  #heirs: 0	  kind:   231
| | -----------------------------	  #heirs: 0	  kind:   35
| N_Extends	  #heirs: 0	  kind:   350
| N_Body	  #heirs: 4	  kind:   334
| | N_Instance	  #heirs: 2	  kind:   375
| | | LOCAL	  #heirs: 0	  kind:   53
 preComment: 0 (***************************************************************************)
             1 (* The two definitions in this standard module are overridden by TLC in    *)
             2 (* the Java class tlc2.module.FiniteSets.  Each operator is overridden by  *)
             3 (* the Java method with the same name.                                     *)
             4 (***************************************************************************)
| | | N_NonLocalInstance	  #heirs: 2	  kind:   376
| | | | INSTANCE	  #heirs: 0	  kind:   50
| | | | Naturals	  #heirs: 0	  kind:   231
| | N_Instance	  #heirs: 2	  kind:   375
| | | LOCAL	  #heirs: 0	  kind:   53
| | | N_NonLocalInstance	  #heirs: 2	  kind:   376
| | | | INSTANCE	  #heirs: 0	  kind:   50
| | | | Sequences	  #heirs: 0	  kind:   231
| | N_OperatorDefinition	*IsFiniteSet	  #heirs: 3	  kind:   389
| | | N_IdentLHS	  #heirs: 4	  kind:   366
| | | | IsFiniteSet	  #heirs: 0	  kind:   231
...
*** End of concrete syntax tree for Module 479

>>mt

External Module Table:
| Module: *ModuleNode: Naturals    uid: 155  kind: ModuleKind  errors: none
| Module: *ModuleNode: Integers    uid: 230  kind: ModuleKind  errors: none
| | Context Entry: Int  232 
| | Context Entry: -.  237 
...

[lemmy]

For starters, we would even need to figure out the module name from the current editor location. Instead, adding all reachable (from the root spec) modules in VSCode's Ctrl+O should address most use cases.

[lemmy]

@peterzeller Do you need more input?

[peterzeller]

@lemmy Sorry for not giving any updates. I'll have some time on the weekend to further work on this.

So far, I have been going through the Java code to see how I can use/extend SANY to get the required information.

Once I figured this out, my next questions would be

1. How to transfer the information to the vscode plugin? E.g. would it make sense to start using lsp4j (which I used in another project and already seems to be used for the debugging support)? Or should I do custom parsing like in SanyStdoutParser?
2. Should I copy+adapt code from the Toolbox implementation or try to extract this to some shared library?

[lemmy]

@peterzeller Thanks for the update! :-)

1. I suggest extending SanyStdoutParser. LSP might strategically be the preferred (@alygin had reasons not to use LSP), and the TLA+ debugger indeed introduced lsp4j in TLC. However, it does not use anything besides the DebugAdapterProtocol, and creating the infrastructure for a server process is a lot of work and might re-encounter tech dept we ran into in the past.
2. For trace expression/exploration, we moved Toolbox code into tla2tools.jar. Would this also make sense in this case?

[lemmy]

FWIW: https://github.com/alygin/vscode-tlaplus/blob/775dbf770a0a182341b68e5af91e5b34965fae0e/src/commands/checkModel.ts#L240-L241 is another use-case where access to SANY's AST would be useful.