Documentation, tutorials, libraries, etc.

[nikswamy]

We've been discussing about consolidating F* libraries, documenting them, refreshing our tutorials etc. in the coming months, e.g., by April 2019. The requirements for this are pretty open ended. Let's use this issue to discuss goals, non-goals and work items towards this task.

• [ ] Converge on a style guide
• [ ] Apply styling conventions to ulib
• [ ] Update our pretty printer to enforce style conventions
• [ ] Document ulib: fsdoc or restructured text?
  • [ ] Standalone sample programs illustrating idiomatic uses of the libraries
• [ ] Refresh online tutorial for F and Low
• [ ] An F* manual, perhaps a reorganization of the wiki
• [ ] Standardization of tool usage: remove seldom used, brittle, or non-standard options

Other things?

Please weigh in with your hopes and desires for documentation.

So far, the discussion included the following people: @aseemr @mtzguido @protz @tahina-pro @catalin-hritcu @danelahman @zoep

[mtzguido]

Linking to #1543 too. Also, I think we should start sending announcements on features/improvements to the mailing list instead of Slack.

[nikswamy]

Notes from a discussion at a group meeting today regarding improving the F* library:

What kinds of improvements do we foresee?

• Settling on a style convention: We should extend https://github.com/FStarLang/FStar/wiki/Style-guide and include documentation style on it too.

• Settling on a documentation tool

  • literate F*?
  • fsdoc? @jaybosamiya says: fsdoc seems to work well enough for common usage. Many like tagged documentation, searchable html etc.

• Focusing effort on most current libraries, deprecating old ones

• Split library into sub-directories?

  • math
  • machine integers
  • state
  • low*
  • legacy
  • experimental ...?

  Might increase discoverability Namespaces instead? per-directory README

  All sub-directories in the include path by default

  Split on different dimensions?

  • experimental
  • legacy

• fsti for all modules

  • older modules don't have fsti

• What about functionality improvements? e.g., making sequences better

  • would be nice, but is also harder ... breaking changes etc.

• Settling on naming conventions

• More discoverability

  • How to find specific lemmas
  • Search utility in emacs mode? Would be nice to have

• Examples of usage

  • Both inlined small usages
  • Example usages at a somewhat larger scale, e.g., see Calc

---

How do we get there?

We hope to make some concrete progress in the next month, presenting improvements to specific modules as exemplars to follow for the rest

• fsdoc and literate F*

  • fsdoc is good for documenting specific, small things, e.g. individual types

  • module-level descriptions

  • What does the combination of literate F* and fsdoc look like

  • @ad-l and @protz had a suggestion, but I failed to record it properly. Would be great if they can fill it in

• Incremental improvements

  • Regularly assigning 1-2 modules to someone and having them improve and present their work at F* meetings,

• What about structural changes like moving things to different directories

  • Broad consensus on splitting on quality, e.g., legacy, experimental etc. Experimental as a staging ground, perhaps some examples move there
  • Splitting on functional lines less important
  • Moving .checked files and .hints files elsewhere <--
  • Aligning namespaces with functionality, e.g., should 'state' be in the name?

• Improving existing code by writing an interface etc. is fair game while the rest settles

[nikswamy]

A proposed revised directory structure (work in progress)

• Rename FStar/ulib to FStar/lib

• A new directory FStar/lib/legacy contains modules that are deprecated

• A new directory FStar/lib/experimental contains modules that will some day make it to the standard library, but are currently still under development and are unstable

• Should modules with native implementations in OCaml or C have names to indicate that?

• In going through all the modules, I came up with the following classes … should they be directories?

  • core
  • native
  • math
  • numeric
  • memory-model
  • effect
  • container
  • reflection
  • tactics I'm mildly in favor of putting things into separate directories (with all sub-directories of lib on the include path) , to help reduce clutter, improve discoverability. But, I wonder if this classification is the right one, what new classes we expect to in the future, etc.? E.g., maybe we'll have a steel directory? maybe some of the memory-model stuff should be in lowstar directory? etc.

See the table in https://github.com/FStarLang/FStar/wiki/Documenting-the-library

[aseemr]

While we are at it, should we also rename HyperHeap and HyperStack modules to be LowStar. instead of FStar.? And FStar.ST --> FStar.Effect.ST?

[denismerigoux]

Renaming FStar.Classical.fsti into Fstar.Squash.Properties is going to cause even more confusion in my opinion. This module is the first you use as a newcomer whenever a proof doesn't go through with SMT. I would expect a name more like FStar.Logic.fst.

[mtzguido]

I was thinking yesterday that the per-functionality split (core, native, math, etc) should probably not be made into directories. It makes it harder to find a module when you know its name (but maybe not its class) and pollutes the include paths (+ introduces a question of precedence). If the only reason for this is to make it easier to discover related functionality, perhaps we need to write and maintain a "roadmap" file, or some kind of marker within each file so they can be listed automatically.

The legacy/experimental split into directories does make sense to me, I would expect them to be left out of the include paths and manually added by users if needed, so they know they are doing something fishy.

I would not mind however to use the directory structure to match the module's namespaces, à la Agda/Haskell.

[msprotz]

The proposal was based on the observation that fsdoc doesn't render nicely when running a file through fstlit. So, right now, this makes it hard to mix fslit and fsdoc together.

The suggestion was to make fslit aware of fsdoc so that when rendering a file via fslist, fsdoc summaries get interpreted as, say, bold text, and the body of fsdoc gets intepreted as regular restructured text.

[nikswamy]

Is that table editable in place for others? If not, maybe I should move it to a wiki page where we can all edit.

Some responses to points raised so far:

• I like the idea of a roadmap/README briefly describing all the files, e.g., by organizing them into different classes.

• I agree FStar.Squash.Properties isn't a great name. I suggested it mainly to call out the similarity to the conventions used for Seq, List, etc. I don't particularly like FStar.Classical---the only thing classical there is the very last excluded_middle lemma. Denis' suggestion of FStar.Logic is okay, but it's also very broad. What about splitting into several modules? FStar.Forall, FStar.Exists, FStar.Implies, FStar.Or (excluded middle could go here), FStar.And, FStar.Equality, … for each of the connectives that this module manipulates.

• I'm also not sure about the status of the LowStar namespace or the FStar.Monotonic namespace. What do they signify? Some attempts:

  • LowStar contains modules that have special extraction status for Kremlin? But, that isn't really correct, since the machine integer modules do not have the LowStar prefix.
  • FStar.Monotonic: modules that make use of witness/recall? Not really, since witness/recall really are tied to the effect, and FStar.Monotonic.Hyper* is pure.

We also have the Steel namespace in another branch. What convention does it represent?

[aseemr]

FStar.Monotonic.?X and FStar.?X should just be merged into FStar.?X (I am to blame for introducing this namespace).

As for LowStar, could we use it for modules that make sense only in the C land? Would HyperStack, HyperStack.ST fall into this category? Machine integers may not since they have OCaml implementation too.

[s-zanella]

As @mtzguido, I believe that splitting files into subdirectories introduces more problems than it solves. It adds new default include paths and creates confusion about their precedence. It also makes it harder to find a module and grep in files. The only advantage I see is that it unclutters ulib a bit. All this would not feel necessary if we had good indexed and browseable library documentation in HTML, or a working built-in search mechanism (e.g. https://coq.inria.fr/distrib/current/refman/proof-engine/vernacular-commands.html?highlight=search#coq:cmd.search)

It still makes sense to move legacy and experimental modules into subdirectories not in the default include path so as to force users of those modules to be conscious about their nature.

I would have a different opinion if there was some relation between filesystem paths and module names, like in Haskell/Agda/Coq (see e.g. https://coq.inria.fr/distrib/current/refman/language/gallina-extensions.html#libraries-and-filesystem).

A last concern about a massive module renaming is upgrading existing code and annoying users. I think it wouldn't take much effort to keep backwards compatibility by preserving existing modules: e.g. if we split FStar.A in FStar.X and FStar.Y, we could keep FStar.A and just include FStar.X and FStar.Y. We can then mark FStar.A as deprecated and nag users into switching to FStar.X or FStar.Y with an appropriate warning (we will need a module deprecation mechanism like suggested in https://github.com/FStarLang/FStar/issues/1673).

[nikswamy]

About a massive module renaming: yes, I was thinking of something like you proposed to not break everyone. The module with the old name would include the new ones, go in the legacy directory, and be deprecated. Thanks also for the reminder to #1673.

[msprotz]

Note that include has no consequence for type-checking but has more consequences for extraction, with extra checked/krml files + the need to update the -bundle options to kremlin.

[msprotz]

As @mtzguido, I believe that splitting files into subdirectories introduces more problems than it solves. It adds new default include paths and creates confusion about their precedence. It also makes it harder to find a module and grep in files. The only advantage I see is that it unclutters ulib a bit. All this would not feel necessary if we had good indexed and browseable library documentation in HTML, or a working built-in search mechanism

Are we proposing subdirectories as a substitute for a README.md or a bit of high-level documentation that would give a tour of ulib, presenting each module and giving a one-sentence summary of what they're supposed to achieve?

This was the intent behind https://fstarlang.github.io/docs/ -- would a more structured version of that landing page suffice?

I am still in favor of moving legacy and experimental files in subdirectories because the intent is that these files should not be discoverable.

[fournet]

Some comments ahead of the discussion:

• Managing expectations: improving the libraries will require a lot of dedicated efforts.
• Why focusing on a one-shot revision of the library structure? For documentation, precedence, deprecating features, etc I'd also rather rely on language-based mechanisms rather than file paths. That said, in several other projects we ended up putting the .fst in other directories.
• Improving the emacs mode or providing some CLI library grep would also help.
• Navigating multiple-module libraries is still hard; for example I never know which file to look up for an aspect of the memory model. Tools to aggregate minimal, documented .fsti irrespective of the underlying module structure would help. (Everparse comes to mind, too.)
• Do we need guidelines for extraction? E.g. which functions should be marked as inline, or as no_extract? Do we need guidelines for include vs open vs qualified access? For recommended module name abbreviations?
• The bar for upstreaming minor improvements is too high. As a consequence, we end up with useful definitions and abbreviations in second-class libraries in other projects. Maybe we could batch their CI/PR review effort?

[jaybosamiya]

For reference, here's the (documentation) style guide that is enforced by Python for their libraries: https://www.python.org/dev/peps/pep-0257/

[nikswamy]

Folks, from https://github.com/FStarLang/FStar/pull/1854 it seems pretty clear to me that we need to significantly improve fsdoc in order to use it to generate reasonably formatted documentation independently from the code of our libraries.

My concern now is that we'll be unable or unwilling to document our libraries until the fsdoc tool improves.

Should we just go ahead and document our libraries in code comments associated with every signature. You can browse the documentation locally, of course, or online using linguist in a browser to make it look at least somewhat pretty.

Welcoming opinions from all, pinging a few. @protz @ad-l @aseemr @denismerigoux @jaybosamiya

[nikswamy]

For generating documentation, would we be better off writing a separate text-processing tool to emit selected parts of a F* module in markdown?

The current fstar --doc implementation parses into the frontend AST and then attempts to print back selected bits while formatting comments and code. Getting that to be perfect still requires quite a lot of work.

[msprotz]

Isn't it what fslit does? It doesn't go through the F* AST, right?

[nikswamy]

yep, that's the fslit model. I'm asking if it makes sense for fsdoc to be similar.

[aseemr]

I would be in favor of not gating the documentation on improvements of fsdoc or some other tool. We can write the documentation in comments now so that we at least have the content, and then we can port it to whichever format we decide to use. If we do so, can we fix some conventions to follow for uniformity.

[jaybosamiya]

Yup, documentation improvements don't need to depend on having improvement on fsdoc yet. If we follow the style that @denismerigoux and I have written for #1854, then it should(?) be fairly straightforward to write a separate tool that can generate markdown/html that looks nice. For an example of how I expect the tool to generate markdown/html output, see the comment there (or alternatively https://gist.github.com/jaybosamiya/05f28d6e34c45b73436a835031346c77 which has working hyperlinks too).

[nikswamy]

See Issue #90 for some other ideas about extending the tutorial

[nikswamy]

See issue #88 for some ideas about marking up and extracting documentation from F* files

[nikswamy]

Would be nice to have a dedicated tutorial chapter regarding normalization