Markus Alexander Kuppe

One idea would be to get rid of `MC.cfg` entirely and extend the approach of [apalache with CInit](https://github.com/konnov/apalache/blob/master/docs/manual.md#parameters). Instead of naming conventions, though, there would be a special module with...

I don't have a complete proposal yet (in this particular case, I could imagine some syntax along the lines of mv == MC!ModelValue). What do you think about the premise...

FWIW: I just spent five minutes figuring out why TLC takes forever to check a small-ish spec. The reason was that the extension settings included TLC's `-dump ...` parameter as...

> How would model values work with the apalache approach? @dricketts https://github.com/tlaplus/tlaplus/commit/f50d67d2169a821989ac0b4250bb2ed04ad4a841

An example of a user having problems with writing a correct TLC config file: http://discuss.tlapl.us/msg04859.html

You can reuse the generated `MC.tla` and `MC.cfg` files in VSCode. If you have two or more Toolbox models `Model_1`, `Model_2`, ..., copy and rename the Toolbox `MC.tla/cfg` files to...

@alygin Is there a way to prevent tabbing until tabbing works reliably? I fear that users accidentally change the semantics of their specs.

Erich Gamma: ["the indentation behaviour is language specific and needs to be provided by a language extension. In this case it is the python extension. Therefore pls report the issue...

Given that `editor.useTabStops` is on by default, our extension should probably raise a warning.

Likely related to make web-views work: https://code.visualstudio.com/blogs/2021/10/11/webview-ui-toolkit Running SANY in WASM could probably be accomplished by using GraalVM: https://www.graalvm.org/