Introducing tlabyexample.com

[Federico Ponzi]

Hello TLA+ community,

I’ve created a small website, https://tlabyexample.com, which aims to let users learn TLA+ interactively by running TLC in the browser with zero installation required. Please check it out and feel free to contribute on GitHub: https://github.com/FedericoPonzi/tla-by-example.

Background: I managed to run tlatools in the browser using the CheerpJ JVM. I first investigated this while working on a web version of the TLA+ formatter (https://gh.fponzi.me/tlaplus-formatter/), which depends on SANY. I later realized it might be possible to run TLC as well.

I quickly put together a PoC here: https://gh.fponzi.me/tlaplus-web/ (repo: https://github.com/FedericoPonzi/tlaplus-web). Having TLC in the browser might not sound exciting for veteran users, but it enables several useful use cases, such as having a playground that requires no local installation, potentially lowering the barrier to entry for newcomers and serving as an interactive sandbox for playing with specs from the Example repo.

Please share any feedback here or open new issues with ideas, suggestions, or fixes.

Thanks,

Federico

[Felipe Oliveira Carvalho]

Looks great!

--
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 visit https://groups.google.com/d/msgid/tlaplus/c0f2fbb8-e95c-4e75-9f66-94926ccdedc0n%40googlegroups.com.

[Markus Kuppe]

This is really great and something many users have been asking for over the years. It's great to see it finally coming together.

Markus

> To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CAOC8YXYK5QHtexJLmVJHgR%2BXt%2B-kg5ZwZuJnir6wyuFGj2Ku7A%40mail.gmail.com.

[Andrew Helwer]

Very exciting! Been wanting to make something like the Lean Natural Number Game but for TLA+ for a while, which this would make possible.

Andrew

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/FEA1D44F-F1C9-4CBE-A9FE-CDB902DA7AD0%40lemmster.de.