Hillel Wayne

Latex builder doesn't emit the `write-started` event

3

### Describe the bug `write-started` is emitted in `Builder.write` ([here](https://github.com/sphinx-doc/sphinx/blob/ace5744b82345150baf3c71d6f47a257c89001ec/sphinx/builders/__init__.py#L582)), but `LatexBuilder` overrides `write` and does not call `super()` ([here](https://github.com/sphinx-doc/sphinx/blob/ace5744b82345150baf3c71d6f47a257c89001ec/sphinx/builders/latex/__init__.py#L273)). ### How to Reproduce In conf, add `extensions = ["foo"]`....

"Check Model with TLC" fails silently if there's no cfg file

1

By fails silently, I mean it doesn't show this popup:  "Check and debug model with TLC" makes the popup appear normally. This is with the most recent version of...

Pluscal translation errors suppressed if there are existing TLA+ errors

1

Spec: ``` ---- MODULE PlusCal ---- EXTENDS TLC (*--algorithm sample_computation variables x = 0; begin print(x); x = 1; end algorithm;*) \* BEGIN TRANSLATION \* END TRANSLATION Foo == x...

https://will62794.github.io/tla-web/

Now that GPT makes it possible to convert between the two with minimal-ish pain *and* I know Sphinx way better, this is more feasible. GPT is probably going to choke...

Feature Request: `update vars` command

4

## Motivation This came up in the Community Outreach meeting as a good potential first "refactoring tool" for TLA+. Given we have the AST, we know 1) all of the...

Should new learning exercises be placed in this repo?

1

https://docs.tlapl.us/learning:exercises

https://rocq-prover.org/about#Name