-
Notifications
You must be signed in to change notification settings - Fork 236
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 isML
, otherwise it isTot
. Your file may or may not be parsed withFStar.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 getsopen Prims
prepended by default. This is not the behavior of files outside of theFStar
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 inulib/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 theProperties
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 inhyperheap
.
JP: putting some questions below that I and others have.
Questions
-
Why do we have so much emphasis on
Seq
instead ofList
? Is it for verification reasons, or just becauseSeq
organically grew to have more lemmas? -
Some naming inconsistencies:
-
FStar.TSet
vsFStar.List.Tot
-
FStar.MRef
vsFStar.Monotonic.RRef
-
From the names it is not obvious that
FStar.Array
works only withFStar.Heap
andFStar.Monotonic.Seq
works only withFStar.HyperHeap
-
Should it be
FStar.Squash.Properties.fst
instead ofFStar.SquashProperties.fst
?