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

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

Closed
kape1395 opened this issue Jan 28, 2024 · 4 comments · Fixed by #325
Closed

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

kape1395 opened this issue Jan 28, 2024 · 4 comments · Fixed by #325
Assignees

Comments

@kape1395
Copy link
Collaborator

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:

@kape1395 kape1395 self-assigned this Jan 28, 2024
@kape1395
Copy link
Collaborator Author

@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
Copy link
Member

lemmy commented Jan 29, 2024

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
Copy link
Collaborator Author

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
Copy link
Member

lemmy commented Jan 30, 2024

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Development

Successfully merging a pull request may close this issue.

2 participants