TLA+ wiki: https://docs.tlapl.us/

Federico Ponzi

unread,

Oct 8, 2024, 1:43:14 PM10/8/24

to tlaplus

Hello,

At https://docs.tlapl.us/, you'll find a new wiki (based on DokuWiki) that we've created as an effort to improve the state of documentation for TLA+ and its tools. We encourage you to register an account and contribute in any way you see fit. If you spot mistakes or think something could be improved, feel free to make updates. Let’s work together to make this resource as valuable as possible!

A big thanks to Markus for helping set up the wiki.

Federico

Calvin Loncaric

unread,

Oct 9, 2024, 1:17:27 AM10/9/24

to tla...@googlegroups.com

Thanks a ton for setting this up!

One quick observation: it seems DokuWiki rewrites the less-than-or-equal operator <= to the arrow ⇐, which makes it hard to write TLA+ inline in text (see e.g. https://docs.tlapl.us/using:standard_lib). Maybe we can disable that conversion?

https://docs.tlapl.us/wiki:syntax#text_conversions

--

Calvin

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8310799e-b497-460a-9c89-f3f1a25a7e5an%40googlegroups.com.

Federico Ponzi

unread,

Oct 9, 2024, 8:19:22 AM10/9/24

to tlaplus

Thanks Calvin, I've updated the wiki's settings to disable the entity rewriting. Please let me know if you spot more issues.