Improve Documentation

[A-Manning]

There is a big lack of clear and easily found documentation for F*. The tutorial is nice but it is still very lacking. After reading through the tutorial, I had no notion of things like fuel, where different modules reside in the source code, etc.

Is this being documented already, or is this something that can be worked on?

[ad-l]

We are aware of the lack of documentation. Our current process is to start using a new tool [1] that generates documentation out of F* modules in the style of ocamldoc. This is still very new (fstar --doc was added today and it is still missing many features) but we will try to document as much of the libraries in ulib/ as possible and make it available on the F* website soon.

[1] https://github.com/FStarLang/FStar/wiki/Generating-documentation-with-fsdoc-comments

[A-Manning]

Great to hear! As somebody relatively new to F*, it's been hard to start out. I don't know the language well enough to know what the simpler stuff would be, but if anybody can point me in the right direction I'd be glad to take some of the low-hanging fruit

[msprotz]

I think we're particularly eager to hear from beginners about the type of information they wish they had, along with the non-obvious things that we no longer notice. We've been trying to put information at https://github.com/FStarLang/FStar/wiki including a "beginners" section -- any suggestions are most welcome.

What do you think of "a tour of the standard library" and "using and understanding fuel"?

[A-Manning]

Both would be fantastic.

The tutorial is a good thing to have - I remember using the "try F#" tutorial a few years ago and being instantly hooked.

It's hard for me to say what's really needed most, but I've spent all day going over F* and I'm still not sure if it has floating numerical types, for example(I'd imagine i doesn't, because accuracy might be an issue with floats). The source code references 'float' and 'double' a lot, but the tutorial example doesn't seem to accept them. I also spent a long time trying to figure out how to cast an Int64, until I found that F* ints have arbitrary precision(to the best of my knowledge).

For something like this to be easy to pick up, which I imagine is a goal of many of the contributors, absolutely everything needs to be documented and catalogued, from the built-in types to the syntax(yes, it's very similar to F# and OCaml, but it still needs to be explained), to hints.

The project needs to be better explained too - I'm still unsure as to what exactly 'Universe' is. I didn't know if there was built-in support for objects until I asked. All of these things need to be made explicit.

Personally I'll be writing a short blog about F* once I get comfortable with it - I've found a lot of F# blogs to have far better explanations of things than the actual documentation, and it's always good to have more than one resource to learn from.

[nikswamy]

@A-Manning: This is really great ... Thank you! A blog sounds very useful indeed. We've also been planning an official F* blog hosted on github as a way for us to document new features/examples that we add regularly.

[msprotz]

@A-Manning : https://github.com/FStarLang/FStar/wiki/Understanding-and-using-fuel

[msprotz]

any comments welcome

[A-Manning]

@msprotz Cheers, that was a great explanation.

[nikswamy]

This is a very open-ended issue. We have a new tutorial, with more material planned. Closing.