Working on a TLC2 (TLA+ model checker) package for Guix, until I found that one of its dependencies is lsp4j (not yet packaged), which is built with Gradle, which is not currently packaged in Guix.
This escalated quickly. I should probably try to build without Gradle. My Java skills are weak, so I guess we'll see how this goes...
I'm pretty excited that I have a working #TLA+ Tools package for #guix working now (tla2tools.jar). But I have a lot of cleanup (for it and new dependencies) to do before offering a patch, and some more wrapper scripts to write. Also need to figure out why some pcal tests are failing.
This allows for model checking, simulation, and LaTeX output generation, among some other things as well.
TLA+ Tools patch series submitted after ~17 hours of work:
https://issues.guix.gnu.org/47789
I'll consider tackling TLAPS (the proof system) in the near future, if I have the energy and it's not too involved.
@mikegerwitz Well done! Java packages aren’t the easiest; bundling binaries (jars) is widespread practice.