diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 6d9efb9..8ed8e85 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -11,10 +11,11 @@ Fork this repository and clone your fork onto your local machine to make modific Test the site and your modifications locally by running: ```zsh -➜ ~ hugo server -D +➜ ~ hugo server --buildDrafts --buildFuture ``` -The `-D` option will show you pages still in draft mode. +The `--buildDrafts` (or `-D`) option will show you pages still in draft mode, and `--buildFuture` (or `-F`) will show you pages with a publication date in the future. +If Hugo isn't serving your post and isn't displaying any errors then you are probably missing one of these two options. ## Writing a blog for the TLA+ website @@ -57,4 +58,4 @@ draft = false 6. Contribute your blog post upstream to this repository using the normal pull request mechanism. -While this website does not make use of all features available in the [Hugo Relearn theme](https://github.com/McShelby/hugo-theme-relearn), you can read its [documentation to learn more](https://mcshelby.github.io/hugo-theme-relearn/index.html). \ No newline at end of file +While this website does not make use of all features available in the [Hugo Relearn theme](https://github.com/McShelby/hugo-theme-relearn), you can read its [documentation to learn more](https://mcshelby.github.io/hugo-theme-relearn/index.html). diff --git a/content/blog/2024-12-dev-update/index.md b/content/blog/2024-12-dev-update/index.md index d175732..6c8a96f 100644 --- a/content/blog/2024-12-dev-update/index.md +++ b/content/blog/2024-12-dev-update/index.md @@ -1,7 +1,7 @@ +++ title = "December 2024 Monthly Development Update" type = "blog" -date = 2024-12-01 +date = 2024-12-15 +++ Hello! diff --git a/content/blog/2025-01-dev-update/index.md b/content/blog/2025-01-dev-update/index.md new file mode 100644 index 0000000..bd45656 --- /dev/null +++ b/content/blog/2025-01-dev-update/index.md @@ -0,0 +1,58 @@ ++++ +type = "blog" +title = 'January 2025 Monthly Development Update' +date = 2025-01-15 ++++ + +You're reading the TLA⁺ Foundation monthly development update. +Here we summarize the past month of development for the benefit of Foundation patrons and interested members of the community. +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. +If your contribution was missed or some important part of it that wasn't captured in the summary, worry not! +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). + +If you're interested in getting involved in the TLA⁺ community: +- Learn TLA⁺ starting [here](https://lamport.azurewebsites.net/tla/learning.html)! +- Read the mailing list [here](https://groups.google.com/g/tlaplus)! +- Join the monthly virtual community meetings [here](https://groups.google.com/g/tlaplus/c/CpAEnrf-DHQ/m/YrORpIfSBwAJ)! +- Start hacking on the tools themselves [here](https://github.com/tlaplus/tlaplus)! + +Let's start with some interesting non-coding-related developments & announcements: +- The [TLA⁺ Community Event 2025](https://conf.tlapl.us/2025-etaps/) talk submission deadline is coming up soon, on February 7th. + The conference will be co-located with [ETAPS 2025](https://etaps.org/2025/) in Hamilton, Ontario, Canada on May 4th, 2025. + Get your submissions in soon! +- 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. + TLA⁺-related submissions are welcome and the submission deadline is also fast approaching, on February 3rd. +- [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. + +Now on to coding-related community developments: +- [Federico Ponzi](https://fponzi.me/) and [Hillel Wayne](https://www.hillelwayne.com/) landed a number of bugfixes in the TLA⁺ VS Code extension, such as [fixing reporting of PlusCal labels](https://github.com/tlaplus/vscode-tlaplus/issues/352). +- [Karolis Petrauskas](https://github.com/kape1395) wrote some fixes for the [TLA⁺ Proof Manager](https://github.com/tlaplus/tlapm) (TLAPM) parser, fixing [a bug](https://github.com/tlaplus/tlapm/pull/189) in the level-checker's handling of quantifier bounds and [another bug](https://github.com/tlaplus/tlapm/pull/191) in the semantic resolver's handling of `USE` statements. + He also updated the TLA⁺ language server (which uses TLAPM's parser) to surface proof obligations [generated by `USE` steps](https://github.com/tlaplus/tlapm/pull/193), and fixed the long-lived [updated_enabled_cdot branch](https://github.com/tlaplus/tlapm/pull/148) to ensure it works with the LSP. +- [Finn Hackett](https://github.com/fhackett) contributed [a fix](https://github.com/tlaplus/tlaplus/pull/1079) supporting the emerging use case of validating implementation logging data with TLC, the inverse of model-based testing where TLC generates traces that the system is driven along. + This requires efficiently reading structured data into TLC, most often using the binary TLC state format. + The [community modules](https://github.com/tlaplus/CommunityModules) expose de/serialization routines for this format. + The fix enabled reading arbitrary string values from the state format, not only those that were generated during initial model checking and thus present in the string interning table. + Finn also proposed an extension from the current ASCII string format to UTF-8. +- Longtime TLA⁺ Tools maintainer [Markus Kuppe](https://github.com/lemmy) collaborated with Andrew Helwer on a PR to support [breakpoint expressions in the TLA⁺ debugger](https://github.com/tlaplus/tlaplus/pull/1099), explored finitizing specifications of monotonic systems, and investigated some fingerprint duplication issues arising during long-running model checking ([1](https://github.com/tlaplus/tlaplus/pull/1119), [2](https://github.com/tlaplus/tlaplus/pull/1115)). + +Finally, things [Andrew Helwer](https://ahelwer.ca/) (author of this post) worked on - all funded by the TLA⁺ Foundation! +- 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). + 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). +- 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/). + 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. + 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! +- 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)). +- 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. + There's even demand from TLC itself for a more flexible SANY API, as we found with the debugger work. + 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. + +## Newbie Corner + +Here we pick one issue to highlight that would be a good choice for new contributors! +This month it's [fixing the PlusCal CLI `-labelRoot` option](https://github.com/tlaplus/tlaplus/issues/1092). +PlusCal is a language that automatically transpiles to TLA⁺. +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. +The fix would require raising an error in the parameter parsing function if the user provides an invalid identifier. + +[Last month's](/blog/2024-12-dev-update/) highlighted starter issue has not yet been claimed; it's also a good choice! +