hwayne / learntla-v2

Learn TLA+ for free! No prior experience necessary!
https://www.learntla.com
Other
185 stars 39 forks source link

How to make a scratch file? #25

Closed louy2 closed 2 years ago

louy2 commented 2 years ago

In the section Setup > Making a Scratchfile, the paragraph only mentions

To do that, I have a separate file I call “Scratch”

Yet how to create this separate file is not mentioned. I started looking for "New File" without success.

There is also a strong relation that a file is a module, so I started looking for "New Module", which I found, but it not mentioned in the guide makes me unsure what to make of it.

Finally I remember that the guide until this point only mentioned creating spec, and creating a separate scratch spec works.

For the scratch spec, the screenshot shows the file name to be lowercase "scratch", but the listed code has titlecase MODULE Scratch which led to an error.

For the scratch model, the screenshot shows the Value box to the bottom, but the text reads "the output of Eval will be put on the box to the right."

hwayne commented 2 years ago

I'll check through everything this week.

jmg-duarte commented 2 years ago

@louy2 So you're not left hanging, here's my textual guide:

I know this isn't much of a guide, but hope it helps!

hwayne commented 2 years ago

Fixed, will push soon!