Re: [tlaplus] REPL enhancements

[Willy Schultz <will62794@xxxxxxxxx>]

> This handles constant-level expressions?

Yeah, basically. Expressions are evaluated in the context of the current definitions in the spec and any CONSTANT instantiations, though I currently didn't add a way to actually instantiate CONSTANT values while using the REPL interface. I don't think that's too critical, though. Personally, I find a large percentage of my REPL usage consists of evaluating constant expressions and maybe also testing out a few manually defined operators.

Note that for evaluating expressions in the context of a current spec state, one can instead use the "Trace _expression_" feature in the web interface, which allows for this.

On Thursday, August 17, 2023 at 7:37:18 PM UTC+1 Andrew Helwer wrote:

Awesome feature, Will! This handles constant-level expressions?

Andrew

On Thursday, August 17, 2023 at 2:06:44 PM UTC-4 Willy Schultz wrote:

Just for reference, I've added a basic REPL prototype into the web-based TLA+ interface/interpreter. Feel free to try it out and see if it may address any of the outstanding REPL feature desires.

On Wednesday, May 19, 2021 at 7:17:45 PM UTC+1 Markus Kuppe wrote:

On 18.05.21 10:34, Markus Kuppe wrote:
> 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.


https://github.com/tlaplus/tlaplus/issues/627


M.

-- 
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/4d83e8aa-0455-4cfd-bc62-faae682004dbn%40googlegroups.com.