|
| 1 | ++++ |
| 2 | +type = "blog" |
| 3 | +title = 'January 2025 Monthly Development Update' |
| 4 | +date = 2025-01-15 |
| 5 | +draft = true |
| 6 | ++++ |
| 7 | + |
| 8 | +You're reading the TLA⁺ Foundation monthly development update. |
| 9 | +Here we summarize the past month of development for the benefit of Foundation patrons and interested members of the community. |
| 10 | +While things did slow down over the holidays compared to [the blockbuster December update](/blog/2024-12-dev-update/), we do have some material to cover. |
| 11 | +If your contribution was missed or some important part of it that wasn't captured in the summary, worry not! |
| 12 | +These newsletters will be published monthly so it's easy to hop on the next train; open an issue [here](https://github.com/tlaplus/foundation/issues). |
| 13 | + |
| 14 | +If you're interested in getting involved in the TLA⁺ community: |
| 15 | +- Learn TLA⁺ starting [here](https://lamport.azurewebsites.net/tla/learning.html)! |
| 16 | +- Read the mailing list [here](https://groups.google.com/g/tlaplus)! |
| 17 | +- Join the monthly virtual community meetings [here](https://groups.google.com/g/tlaplus/c/CpAEnrf-DHQ/m/YrORpIfSBwAJ)! |
| 18 | +- Start hacking on the tools themselves [here](https://github.com/tlaplus/tlaplus)! |
| 19 | + |
| 20 | +Let's start with some interesting non-coding-related developments & announcements: |
| 21 | +- The [TLA⁺ Community Event 2025](https://conf.tlapl.us/2025-etaps/) talk submission deadline is coming up soon, on February 7th. |
| 22 | + The conference will be co-located with [ETAPS 2025](https://etaps.org/2025/) in Hamilton, Ontario, Canada on May 4th, 2025. |
| 23 | + Get your submissions in soon! |
| 24 | +- East of the Atlantic, [ABZ 2025](https://abz-conf.org/site/2025/) - the 11th International Conference on Rigorous State-Based Methods - will take place from June 10th to 13th of 2025 in Düsseldorf, Germany. |
| 25 | + TLA⁺-related submissions are welcome and the submission deadline is also fast approaching, on February 3rd. |
| 26 | +- [Murat Demirbas](https://cse.buffalo.edu/~demirbas/) wrote [a nice blog post](https://muratbuffalo.blogspot.com/2024/12/exploring-naiadclock-tla-model-in-tla.html) about using [tla-web](https://will62794.github.io/tla-web/#!/home?specpath=.%2Fspecs%2FTwoPhase.tla) to learn & explore an unfamiliar TLA⁺ spec. |
| 27 | + |
| 28 | +Now on to coding-related community developments: |
| 29 | +- [William Schultz](https://will62794.github.io/) has been doing some work on tla-web (to be filled in) |
| 30 | +- [Federico Ponzi](https://fponzi.me/) and [Hillel Wayne](https://www.hillelwayne.com/) landed a number of bugfixes in the TLA⁺ VS Code extension (to be filled in). |
| 31 | +- [Karolis Petrauskas](https://github.com/kape1395) wrote some fixes for the [TLA⁺ Proof Manager](https://github.com/tlaplus/tlapm), focused on the level-checker and the language protocol server used for checking proofs in the TLA⁺ VS Code extension. |
| 32 | +- [Finn Hackett](https://github.com/fhackett) contributed [a fix](https://github.com/tlaplus/tlaplus/pull/1079) enabling ??? |
| 33 | + |
| 34 | +Longtime TLA⁺ Tools maintainer [Markus Kuppe](https://github.com/lemmy) had a number of notable work items: |
| 35 | +- Collaborating with Andrew Helwer on a PR to support [breakpoint expressions in the TLA⁺ debugger](https://github.com/tlaplus/tlaplus/pull/1099) |
| 36 | +- To be added |
| 37 | + |
| 38 | +Finally, things [Andrew Helwer](https://ahelwer.ca/) (author of this post) worked on - all funded by the TLA⁺ Foundation! |
| 39 | +- The December community meeting had a long & spirited discussion about the future of the various TLA⁺ parsers (mostly about whether to transition all tools onto a single parser), so I attempted to capture these thoughts in [a long RFC](https://github.com/tlaplus/rfcs/issues/16). |
| 40 | + I also opened [a RFC](https://github.com/tlaplus/rfcs/issues/17) to get the ball rolling on standardizing the TLA⁺ file format, which in turn led to questions about the standardization process itself which I tried to summarize [here](https://github.com/tlaplus/rfcs/issues/1#issuecomment-2565920953). |
| 41 | +- December was all about getting familiar with the *semantic* part of the Java-based TLA⁺ parser, called SANY; I was already familiar with the syntax part due to past work [adding support for Unicode math symbols](https://ahelwer.ca/post/2024-05-28-tla-unicode/). |
| 42 | + To that end I collaborated with Markus Kuppe to add support for [breakpoint expressions in the TLA⁺ debugger](https://github.com/tlaplus/tlaplus/pull/1099), which required the novel functionality of adding new expressions to an existing model, at runtime. |
| 43 | + Beyond the actual value of the feature itself this was very helpful for developing my understanding of SANY's semantic & level-checking components, and even offered a tantalizing glimpse into the next level - the interpreter! |
| 44 | +- I contributed some minor fixes to SANY such as removing some annoying global static state ([1](https://github.com/tlaplus/tlaplus/pull/1100), [2](https://github.com/tlaplus/tlaplus/pull/1101), [3](https://github.com/tlaplus/tlaplus/pull/1106)) and converting some existing unit test corpuses to use JUnit's parameterized test functionality ([1](https://github.com/tlaplus/tlaplus/pull/1107), [2](https://github.com/tlaplus/tlaplus/pull/1108)). |
| 45 | +- I [started prototyping](https://codeberg.org/tlaplus/simple-checker/src/commit/5641793467fafcf86b261be3db6e6d39a21a658f/app/src/main/java/us/tlapl/Parser.java) what a modern SANY API would look like; with the discussion of transitioning TLAPM onto SANY, and with two existing consumers from [Apalache](https://github.com/apalache-mc/apalache/) and the [tlaplus-formatter](https://github.com/FedericoPonzi/tlaplus-formatter), the day is dawning where SANY isn't just something used by the TLC model-checker. |
| 46 | + There's even demand from TLC itself for a more flexible SANY API, as we found with the debugger work. |
| 47 | + This month will be all about building a semantic test corpus to drive the design of this API, which I hope will be finalized shortly thereafter. |
| 48 | + |
| 49 | +## Newbie Corner |
| 50 | + |
| 51 | +Here we pick one issue to highlight that would be a good choice for new contributors! |
| 52 | +This month it's [fixing the PlusCal CLI `-labelRoot` option](https://github.com/tlaplus/tlaplus/issues/1092). |
| 53 | +PlusCal is a language that automatically transpiles to TLA⁺. |
| 54 | +The CLI exposes a few parameters to control this output, and one of them determines the name of the root next-state relation; this parameter wrongfully accepts arbitrary string input instead of ensuring the given name is a valid TLA⁺ identifier. |
| 55 | +The fix would require raising an error in the parameter parsing function if the user provides an invalid identifier. |
| 56 | + |
| 57 | +[Last month's](/blog/2024-12-dev-update/) highlighted starter issue has not yet been claimed; it's also a good choice! |
| 58 | + |
0 commit comments