Editing files in the library

F★'s standard library currently resides in ulib (as in universes). The lib directory contained the old (stratified) standard library. See https://github.com/FStarLang/FStar/blob/master/src/README to make sure you don't get confused between the (old) stratified code and the (new) universes code. The former is now mostly gone, so we might want to remove this comment and might consider renaming ulib back to lib.

Here are some tips&tricks if you plan to edit these files and/or submit a pull request.

F★ language quirks.

• Always annotate your top-level functions with a val (because #517, #620, #581).
• Always provide the return effect for your functions! The default effect changes in an unpredictable manner; if FStar.All is in scope, then the default effect is ML, otherwise it is Tot. Your file may or may not be parsed with FStar.All in scope, depending on the (unspecified) ordering of files performed by the dependency analysis and the criterion below.
• If your module is in the namespace FStar, then it only gets open Prims prepended by default. This is not the behavior of files outside of the FStar namespace! See Dealing with F★ dependencies for more information.
• If your module uses the HyperHeap memory model, then you need to append the .fst file to the list of files in the HYPERHEAP variable in ulib/Makefile. Otherwise, regression testing will typecheck it using plain Heap and fail.

General recommendations

• The naming convention is in flux. Stay tuned for some consensus, hopefully soon (see #687).
• Seq, Set, Map, OrdMap, OrdSet contain a minimalistic interface. It is recommended to use the Properties module (e.g. Seq.Properties) to write lemmas / extend these modules.
• My understanding is that the hyperheap folder is only meant to contain modules that must be overridden via --include path/to/hyperheap. In clear, no new files should be created in hyperheap.

JP: putting some questions below that I and others have.

Questions

• Why do we have so much emphasis on Seq instead of List? Is it for verification reasons, or just because Seq organically grew to have more lemmas?

• Some naming inconsistencies:

• FStar.TSet vs FStar.List.Tot

• FStar.MRef vs FStar.Monotonic.RRef

• From the names it is not obvious that FStar.Array works only with FStar.Heap and FStar.Monotonic.Seq works only with FStar.HyperHeap

• Should it be FStar.Squash.Properties.fst instead of FStar.SquashProperties.fst?