Re: [tlaplus] TLA+ Package Manager?

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.

On Tue, May 12, 2026 at 7:41 PM thomas...@xxxxxxxxx <thomasgebert@xxxxxxxxx> wrote:

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.