FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.68k stars 232 forks source link

module Welcome from the tutorial is not in source tree #1551

Open valera-rozuvan opened 6 years ago

valera-rozuvan commented 6 years ago

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.

valera-rozuvan commented 8 months ago

Is still relevant? Has the contents of module Welcome been moved to a GitHub repository somewhere?