4 ms·

I've considered using the command-line when I started using TLA+, but the manual discouraged it and I use it only occasionally so I didn't want to invest too mu

I've considered using the command-line when I started using TLA+, but the manual discouraged it and I use it only occasionally so I didn't want to invest too much time on it. I'd love to see a TLA+ package for vscode [1]. It seems there is more and more TLA+ adoption, it is surprising there aren't better environments to use it. The TLA Toolbox is awful (well, to be fair to the people that developed it, it does the job and maybe it's ok for some category of users). EDIT: [1] there's one actually, https://github.com/TeamTilapia/vscode-tilapia https://github.com/TeamTilapia/vscode-tilapia

RBerenguel 8y ago
Thanks for the link. I always prefer emacs above anything, but VS Code is not bad at all.
- yodsanklai 8y ago
  It doesn't seem to be maintained, and it's not packaged either. Not sure it's worth installing.
pron 8y ago
I like the Toolbox. - It shows you the ASCII and pretty printed spec side-by-side. - It plots TLC data as it runs and presents live coverage data in a nice way. Soon it will also show TLC performance profiles as color maps. (https://twitter.com/lemmster/status/1082787089140183040 https://twitter.com/lemmster/status/1082787089140183040) - It makes running TLC in the cloud (single-node or distributed) very easy. (https://tla.msr-inria.inria.fr/tlatoolbox/doc/cloudtlc/ https://tla.msr-inria.inria.fr/tlatoolbox/doc/cloudtlc/) - I don't know of any other way of using TLAPS. (https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/A_simple_proof.html https://tla.msr-inria.inria.fr/tlaps/content/Documentation/T...) Then again, I'm really not a fan of either vim or emacs, despite having used the latter as my main editor for some years. I think this may be because I value tools that present more information in a convenient way that allows me to inspect and analyze my text over tools that allow editing more quickly (when I write code, I spend 80% of my time in Sourcetrail and only use the editor to punch-in characters), but I don't know.
- aseipp 8y ago
  I think it's mostly just sticker shock. Downloading another thing, and it's a bit spoiling these days when most toolsets have some amount of cross-editor support. You can do similar things in various language modes in VS Code, after all (plotting/fancy rendering/cloud APIs). There don't seem to be many developers working on TLA+ outside of Microsoft Research though, so I think their work is probably better spent elsewhere than just recreating the Toolbox in other editors. It's not that bad. Maybe in a year or two if TLA+ continues growing in popularity someone will help hash out an alternative. In a prior project one of our developers checked their models in the Toolbox originally and then we just ran them in CI from the command line, which also worked fine and made it easier if people wanted to run/edit them "by hand" in vim or something.
  - deleted 8y ago
    [deleted]

RBerenguel 8y ago

Thanks for the link. I always prefer emacs above anything, but VS Code is not bad at all.

yodsanklai 8y ago
It doesn't seem to be maintained, and it's not packaged either. Not sure it's worth installing.

pron 8y ago

I like the Toolbox. - It shows you the ASCII and pretty printed spec side-by-side. - It plots TLC data as it runs and presents live coverage data in a nice way. Soon it will also show TLC performance profiles as color maps. (https://twitter.com/lemmster/status/1082787089140183040 https://twitter.com/lemmster/status/1082787089140183040) - It makes running TLC in the cloud (single-node or distributed) very easy. (https://tla.msr-inria.inria.fr/tlatoolbox/doc/cloudtlc/ https://tla.msr-inria.inria.fr/tlatoolbox/doc/cloudtlc/) - I don't know of any other way of using TLAPS. (https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/A_simple_proof.html https://tla.msr-inria.inria.fr/tlaps/content/Documentation/T...) Then again, I'm really not a fan of either vim or emacs, despite having used the latter as my main editor for some years. I think this may be because I value tools that present more information in a convenient way that allows me to inspect and analyze my text over tools that allow editing more quickly (when I write code, I spend 80% of my time in Sourcetrail and only use the editor to punch-in characters), but I don't know.

aseipp 8y ago
I think it's mostly just sticker shock. Downloading another thing, and it's a bit spoiling these days when most toolsets have some amount of cross-editor support. You can do similar things in various language modes in VS Code, after all (plotting/fancy rendering/cloud APIs). There don't seem to be many developers working on TLA+ outside of Microsoft Research though, so I think their work is probably better spent elsewhere than just recreating the Toolbox in other editors. It's not that bad. Maybe in a year or two if TLA+ continues growing in popularity someone will help hash out an alternative. In a prior project one of our developers checked their models in the Toolbox originally and then we just ran them in CI from the command line, which also worked fine and made it easier if people wanted to run/edit them "by hand" in vim or something.
- deleted 8y ago
  [deleted]