LSP: Share module search paths between the TLAPS and SANY.

[kape1395]

The TLAPS LSP server should support path sharing both ways:

• TLAPS could provide its path to the vscode extension.
• Also, the TLAPS has to consider paths configured in the extension.

Maybe related to:

• https://github.com/tlaplus/tlaplus/issues/490
• https://github.com/tlaplus/tlapm/issues/3

[kape1395]

@lemmy, what do you think of this plan:

• I build a class in the extension which maintains the paths. The TLC, SANY, and TLAPS then use the paths.
  • User can add path entries via configuration property. There is no such currently, so I would add one.
  • TLAPS would supply its stdlib path "automatically" if installed and enabled.
  • TLA Tools would supply its internal modules as well.
  • Community modules could be handled in a special way here. It could be downloadable on a user click.
• Also, I add a tree view in the side pane to show these paths. Later, we can add modules provided by each path, improving the visibility of existing modules.

I have to solve this for the TLAPS integration, because it will fail if some non-TLAPS-stdlib modules are used in a spec. Also, I have to use these paths if I want to integrate the SANY parser in the TLAPS LSP server for better error messages.

[lemmy]

Sounds good to me assuming you are proposing to let the extension be the "facilitator of paths" between the various tools. How the tools make use of the path information is then up to the tool. For example, TLAPS adds its path information to the extension, and TLC is given this information when it launches.

What are the precedence rules WRT a tool's default lookup path and the extension's configuration property?

[kape1395]

What are the precedence rules WRT a tool's default lookup path and the extension's configuration property?

I think the tool should prioritize its internal library (e.g., the TLC prioritizes the modules contained in tlatools.jar). Other paths are passed as additional search paths. Hopefully, that will not be a problem when some TLAPS modules are moved to the community modules repo.

[lemmy]

This might require tool changes as, IIRC, a library path that is passed to TLC takes precedence over TLC's internal library path.