tlaplus / vscode-tlaplus

TLA+ language support for Visual Studio Code
MIT License
357 stars 33 forks source link

tlc with NixOS #180

Closed err0r500 closed 3 years ago

err0r500 commented 3 years ago

Hello, If I try to use the extension installed with vscode-utils.extensionsFromVscodeMarketplace (in configuration.nix), checking the model generates files in the ./states folder but they get deleted instantly once the check is finished.

Not sure if there are lots of NixOS users here, but do you have an idea what could cause this ? The rest works fine (sany, tla2tex) ; also, tlc works fine in the terminal

lemmy commented 3 years ago

What does this have to do with NixOS and why would you want to keep TLC's temporary data?

err0r500 commented 3 years ago

I was about to edit the question, the problem is that no result is displayed (and I thought it came from the deleted files in states).

Here's the NixOS related problem : I've got 2 ways to install vscode extensions : globally or per user (I can't mix these 2 install modes). The problem I describe happens only if I install the extension globally, everything works fine if I install it as a user. So why don't I just keep it like that ? Because liveshare only works if installed globally... and I'd prefer not to choose between tlaplus & liveshare...

lemmy commented 3 years ago

Sounds to me as if states is a red herring -- TLC deletes temp files in states after execution.

err0r500 commented 3 years ago

The main difference I know between the 2 install modes is that the extension install dir is read-only with global install. I didn't see writes while quickly browsing the extension code, but maybe I missed something ?

lemmy commented 3 years ago

TLC seems to succeed to create states itself, no?

err0r500 commented 3 years ago

yeap, but states is in the spec folder, I meant the installation dir of the extension itself (~/.vscode/extensions/<ext-name> in most distros)

kubukoz commented 3 years ago

@err0r500 you might actually be having the same problem I was having - check out #196.

I'm using home manager and this is my workaround (using a local clone of the repository with the branch #196 is created from checked out).

tla = pkgs.vscode-utils.buildVscodeExtension rec {
# I had to run `npm install` in there first - less than ideal, but it works...
  src = ../../IdeaProjects/vscode-tlaplus;
  name = "vscode-tlaplus";
  publisher = "alygin";
  vscodeExtUniqueId = "${publisher}.${name}";
  version = "1.5.2";
}
alygin commented 3 years ago

The fix is released in v1.5.3. @err0r500, feel free to reopen the issue if the extension still doesn't work on NixOS.