This repository was archived by the owner on Jul 2, 2022. It is now read-only.
Inline interactive/executable TLA+ #105
Description
My understanding is that you are working on an overhaul of this site, so I am posting this note as a possible feature you might be interested in including in the next version.
The tla-web tool implements a fully browser based TLA+ evaluator/interpreter. It might be cool for certain pages of the site to embed interactive/executable TLA+ specs/snippets inline. The Lean theorem prover tutorials have something similar.
The current version of the tool probably isn't quite suitable for embedding elsewhere yet, but it shouldn't be hard to make a simple interface/API to allow this. Just thought I'd make you aware of this as a possibility.