FStar
FStar copied to clipboard
module Welcome from the tutorial is not in source tree
When you access the tutorial found at https://www.fstar-lang.org/tutorial/, the first module you see in the right pane is module Welcome. However, the text:
module Welcome
(*
This interface allows you to edit and typecheck F* programs.
For convenience, you can resize both the tutorial and F* output frames.
Click on the border between frames and drag your pointer to resize.
Any change you make on the editor is automatically saved in your browser.
Your local state gets restored each time you load the tutorial, until your browser data is cleared.
Use the ► button to ask F* to verify the contents of the editor.
This editor lets you work on multiple 'files' at the same time.
Click on the green button in the bar below the editor to create a new tab.
Files can be deleted with the red cross icon next to their name.
Be careful when deleting a tab! Its contents are permanently deleted.
This online interface is only provided to verify the tutorial's simple examples.
To verify complex programs using F*, please install it on your local machine.
*)
is not stored inside the GitHub repository. How can one propose changes/fixes to it?
For example the line:
Your local state gets restored each time you load the tutorial, until your browser data is cleared.
can be split in 2 lines, so that it doesn't go off screen.
Is still relevant? Has the contents of module Welcome been moved to a GitHub repository somewhere?