Open klinvill opened 3 years ago
While using the prompt would be nice for cases where you only have a few constants (like above), it might get unwieldy for specs with many constants. This could be partly improved by persisting previous assignments at a project level. Would it be better to supply initial context by reading in constants from a config file?
There is already TLC's config file (YourSpec.cfg
), and I don't think TLA+ values should be persisted as project-level VSCode settings. Perhaps, it would be useful to generate a more complete YourSpec.cfg
? Right now, the VSCode extension just generates CONSTANT
, INIT
, NEXT
. However, we cannot write INSTANCE ATD WITH N <- 42
in YourSpec.cfg
, thus we probably want MC.tla/MC.cfg (see https://github.com/alygin/vscode-tlaplus/issues/159).
On second thought, my initial observation (this issue) wasn't a good one. Sorry, I should have thought this through.
I agree, I think it makes sense to take advantage of a more complete config like the MC approach you mention. In that case, I'd vote for deferring this until after issue 159 is resolved
Original observation from @lemmy: