[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] REPL enhancements
On 18.05.21 10:10, Christopher Pacejo wrote:
Hi, I'm very excited to see that a REPL has been added last year.
However it doesn't appear to have been developed much since then beyond
the basic expression evaluation functionality in the initial import.
Would I be stepping on any toes if I started working on some enhanced
functionality for it? I have a few ideas I've been kicking around in a
hacky shell-script-based REPL I made a few years ago that I'd be
interested in porting over. Namely:
1) The ability to define operators and instantiate modules.
2) The ability to declare variables, and initialize and update them (one
iteration) via a specified predicate and user input to resolve
nondeterminism (as with TLCExt!PickSuccessor).
3) The ability to define constants (same as in a TLC config file) to
support model values, and extending modules which declare constants.
4) The ability to modify, list, and save to file what's been defined in
the session.
I think these enhancements would help make the REPL a really useful tool
for those learning the language, or those wanting to test and explore
functionality of modules they are developing.
Hi Chris,
to the contrary, we would very much welcome enhancements to the REPL.
Can you please open an issue as a place to discuss technical details?
Some of what you propose is already possible. Other enhancements
probably need a closer look because of restrictions in TLC.
Thanks,
Markus
--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e1816ff4-e7de-16f5-195d-a01e623a66ed%40lemmster.de.