Comments (4)
@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.
from vscode-tlaplus.
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?
from vscode-tlaplus.
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.
from vscode-tlaplus.
This might require tool changes as, IIRC, a library path that is passed to TLC takes precedence over TLC's internal library path.
from vscode-tlaplus.
Related Issues (20)
- Show model/spec name in VSCode status bar
- "Check Again" no-op if TLA+ debugger currently running HOT 1
- Error-Trace modification/addition annotations broken HOT 6
- Check model with TLC is a no-op if there is no PlusCal in the file HOT 2
- Check Again should reuse the current window HOT 3
- Add Wiki documentation for TLC options HOT 3
- Using the extension with remote-ssh HOT 1
- "Output" tab on top of "Errors" tab
- Rename second column of states table from "Diameter" to "Depth" HOT 1
- The `tlaplus.tlaps.check-step` key-binding breaks VSCode's "go to line number" binding HOT 2
- Is there a way to add invariants as in the GUI? HOT 3
- Variables not working as Watch expression HOT 6
- LSP: Document annotations are sometimes lost. HOT 2
- LSP: TLAPS integration makes the IDE crash sometimes. HOT 1
- LSP: Proof step decorations look too distractive. HOT 1
- LSP: Add option to download the TLAPM/LSP.
- Merge "alygin.vscode-tlaplus" and "alygin.vscode-tlaplus-nightly" on Marketplace HOT 3
- Support ANSI escape sequence in trace explorer web view HOT 2
- VSCode status panel stuck in computing initial states when using simulation mode HOT 3
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from vscode-tlaplus.