Provide the content of https://lamport.azurewebsites.net/tla/tla2-guide.pdf in a more accessible, web-friendly format

[lemmy]

Several users such as @ibrhmkoz and @ajdavis have asked to make the content of https://lamport.azurewebsites.net/tla/tla2-guide.pdf available in a more web-accessible format, to improve readability and accessibility online.

Requirements/TODOs:

• Obtain source material tla2-guide.tex.txt from Lamport
• Choose a target format (e.g., Markdown, reStructuredText, AsciiDoc, etc.). The TLA+ project exclusively uses Markdown, but @hwayne can probably provide guidance if needed
• Convert to target format. @ibrhmkoz and @ajdavis can you take this on?
  • Make the origin clear (author of the original .tex version is Leslie Lamport)
• SLC, particularly @muenchnerkindl, to review the proof section of the document, as per Lamport's request
  • Section 8.3 - Temporal Proofs
  • Section 6 - Deprecating/removing named subexpression

[ahelwer]

So are we standardizing on docs.tlapl.us and mediawiki or not?

P.S. @FedericoPonzi could you make me an admin of the mediawiki instance? I'm currently the most prolific user I believe. I would like to lock down registrations so they require manual approval, as otherwise the risk of vandalism is very high.

[lemmy]

So are we standardizing on docs.tlapl.us and mediawiki or not?

Setting aside the technical details, I think it makes sense to have a slightly higher standard for changes to this type of content, especially since it's under the "jurisdiction" of the SLC.

[FedericoPonzi]

(sorry for the OT)
@ahelwer Done, you're an admin now

I would like to lock down registrations so they require manual approval, as otherwise the risk of vandalism is very high.

I think the last time we discussed this, we agreed to leave registrations open for now, and change it later should we get any vandalism. I get an email update on every change, and so far (crossing fingers) we haven't seen any vandalism, so I don't see a reason to lock them down.

[ahelwer]

I'm a bit leery of having documentation scattered across a few websites, but it can make sense if the demarcations are appropriate. @ajdavis mentioned reading a good post about the purpose of documentation, which should satisfy 3-4 purposes (might be referencing this or this but there are a few related things online):

1. Tutorials (learning-oriented)
2. How-to guides (problem-oriented)
3. Explanation (understanding-oriented)
4. Reference (information-oriented)

There's a four-square representation of how these relate but idk whether it helps understanding lol:

So I think as long as we can agree on these demarcations as they apply to TLA+ and only put content neatly falling into a particular category on singular websites, it can be okay to scatter documentation (although we should have a singular root website that directs users to the appropriate category).

The particular document under discussion (the TLA+ 2 language guide) neatly falls into the reference category. However, I'm not sure it is a good choice of first document to convert. As someone who has consulted it many times while writing parsers and tests for those parsers, it seems primarily aimed at TLA+ implementers instead of users. Perhaps the Summary of TLA+ document would be a better initial target?

[lemmy]

@ibrhmkoz specifically requested tla2-guide.tex. However, there's no reason not to also convert summary-standalone.tex. As with all newly created material, proper attribution and indication of the original source must be included.