For my 2 cents, if you have the time, it would be interesting to see how the tool ends up.
That is, I wouldn't expect any particular adoption, and I would focus on what you need from the tool first and foremost w/ small and simple dev effort. This space is super complicated and people will have all sorts of contradictory needs (Andrew does a good job of setting realistic expectations). If something broadly useful comes out, nice. If it scratches your itch and entertains you OSS wise but no one picks it up... still ok, and maybe we learn something. Somewhere in the middle, there's a "boring" tool that helps for some simple/common cases, and can be ignored outside its scope. I'd be happy to learn about any of these outcomes.
On another front, if automating some simple TLA+ transformations/analysis is the name of the game, I have been working on a library-form version of TLC for a little while, and I could make it available for your use. It's a Scala library and loads the TLC codebase, so not exactly that Rust prototype (though don't assume you'd have to ship a .jar). On the flipside, the library links with full SANY, and can broadly interfere with TLC's function in all sorts of fun ways: hooking into module lookups, scanning the AST + module hierarchy, doing thread/restart-safe custom _expression_ / state evaluation (not that you probably need that last one). Feel free to message directly if interested. It will ultimately be an OSS project on our lab's Github, I'm just slow / dealing with a related academic paper submission. No pressure to try it, just kinda related. This paragraph and the one above are orthogonal.
Best,
-Finn
Nobody has yet tried to tackle this problem. TLA+ specs usually benefit from being terse so pulling in dependencies has not being much of a priority; duplicating the spec with copy & paste has sufficed (aka “vendoring” the dependency in corpspeak).
It’s also tricky because the package management design space is quite large and varies from always just pulling the latest version of a given package name and its dependencies (Arch Linux, macOS homebrew) to fully specifying and pinning the transitive dependency graph (nix, guix). Given that TLA+ is occasionally published in papers, that model exploration order (and thus counterexample) can vary by TLC version, and that whether a proof discharges correctly can vary by TLAPM version, it would make sense for a hypothetical package manager to be more on the nix/guix side of things. However that is just my opinion.
Andrew Helwer
I have been writing a spec, and I have been referencing the TLA+ community modules.
Right now I'm just manually copying and pasting the specs into my project so that I can use them later, but I was curious if there had been any effort in making a TLA+ package manager so that modules can be more easily shared and referenced.
I got Claude to hack something together tonight, where it does a pretty basic recursive search of a deps.json (pointing to git repos) in Rust and use tree-sitter to rename the downloaded modules to have their folder namespace.
It seems to work but I have fairly strong objections to pushing AI generated code to GitHub; I would rather write a "correct" version with my own fingers, based on any kind of community input.
That is, unless someone has already done this work so that I don't have to?
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/914eb0ca-0ebb-4f10-a0b6-0d0aecb8cd20n%40googlegroups.com.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUUAFjmtwW%2Bo3O_MYS3MqVo00Do4QE_z%2Bv0%3DtJ%3D6JXgJag%40mail.gmail.com.