Wrote January 2025 development update post

Also changed December 2024 development post publication date Also added note about Hugo CLI option that tripped me up Signed-off-by: Andrew Helwer <[email protected]>
tlaplus · Jan 15, 2025 · e993d43 · e993d43
1 parent 4713698
commit e993d43
Show file tree

Hide file tree

Showing 3 changed files with 63 additions and 4 deletions.
diff --git 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).
+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
@@ -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
@@ -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!
+