Improving the usability of F* (master issue!)

[msprotz]

• move the Low* libraries under the LowStar prefix (instead of FStar)
• remove old libraries from ulib/
• F* doc (the tool) (Implement fsdoc #634)
• write, generate and nightly-rebuild+upload documentation for F*'s ulib
• wiki page that documents a typical workflow:
• the "moving admit" strategy, and general pitfalls when starting with F* (e.g. z3 does not report the first error)
• how to debug "unknown assertion failed", how to read cryptic F* error messages with TOP in the middle, unknown assertion failed because no noeq, confusion if no open FStar_Mul, etc.)
• cheap functors to remove the duplication for integer types (see Cheap functors proposal)
• proper pretty-printer for types (good for F*doc) (Better pretty printer #36)
• naming conventions and design principles for the standard library -- create a wiki page (foo_of_x vs x_to_foo and x_as_foo) (See also Editing-files-in-the-library)
• fix the compiler so that it bootstraps, which will in turn allow
• removing lib/ and contrib/
• fix the confusion between src/basic and lib/
• update tutorial (Update tutorial text for Universes #627)
• have fstar --compile which takes care of extracting + calling ocaml with the right voodoo (e.g. running the right make command in ulib/ml depending on --use_native_int and whether HyperHeap is used or not) and right cmxa
• fix the terrible Fstar.Mul problem by switching to a unicode lexer and advertising × everywhere
• Add *printf-like functions to the standard library (see Add *printf-like functions to the standard library #637)

[Update 2016-11-22] Tahina added more tasks in a comment below #614 (comment)
[Update 2016-11-22] Catalin: moved that discussion to separate issue (#770) about POPL release.

[jkzinzindohoue]

What are the Low* libraries ? Are FStar.HyperStack, FStar.HST and FStar.Buffer part of it ?

[msprotz]

I would say: at least machine integers and buffers. Unclear about HST... maybe.

[jkzinzindohoue]

I think that the machine integers are independent from Low*. They define native OCaml integers for instance.

[msprotz]

Maybe rename it Machine then? From the discussion with @KAepora, the goal was to group modules that "belong together" under a common namespace. It feels to me like machine integers, buffers, hst all talk about very concrete concerns, and should be grouped together... @KAepora happy to have your opinion on this

[jkzinzindohoue]

So the standard library will no longer be unified under the FStar name ?

[nadimkobeissi]

@jkzinzindohoue:

So the standard library will no longer be unified under the FStar name ?

There's nothing here that implies that the standard library would no longer be unified under FStar and that is indeed not a good idea. The point is to organize the FStar standard library in a namespace-based hierarchy. Clearly everything that comes as a core part of FStar, through its standard library, thus belongs under the FStar global namespace. non-FStar top-level namespaces are therefore reserved to third party modules or independent projects.

@msprotz:

From the discussion with @KAepora, the goal was to group modules that "belong together" under a common namespace.

To make this more concrete, the aim is to group modules first by functionality and then by use-case: FStar.Functionality.UseCase. For example, modules dealing with bytes should go under FStar.DataTypes.UInt, from which you can then call, say, a type Uint8.

Notice that this goes against organizing the libraries based on their internal codenames. I would recommend against organizing things in the format FStar.LowStar, or FStar.HST, because this does not lead to a namespace hierarchy that can be intuitively used by the programmer to find the functionality they're looking for inside the standard library. Compare that to something like FStar.Arithmetic.SclarMult.

If we follow my suggested approach, we obtain a namespace that is intuitive to programmers, that helps establish standards that allow us to keep an eye on implemented functionality so that things don't get reimplemented several times.

[msprotz]

@KAepora can you suggest a consistent naming scheme for the modules in ulib? happy to implement any good suggestions

[beurdouche]

Can we add to this list a way to have a monad agnostic IO for debugging code ?
We currently proceed by adding Printfs in the extracted code directly (which is better in case of an extraction bug) but being able to do something like that directly in the F* code without having to care (much) about the typechecker would be faster. Or do we have a better debugging workflow ?

[s-zanella]

Is FStar.IO.debug_print_string what you're looking for?
Some support for *printf-like formatting would be nice.

(* 
   An UNSOUND escape hatch for printf-debugging;
   Although it always returns false, we mark it
   as returning a bool, so that extraction doesn't
   erase this call.

   Note: no guarantees are provided regarding the order 
   of evaluation of this function; since it is marked as pure, 
   the compiler may re-order or replicate it.
*)
val debug_print_string : string -> Tot bool

[msprotz]

Now that we have universes we could theoretically implement a perfectly dependent printf, except that the normalizer would have to be able to reduce functions on strings.

[auduchinok]

Speaking about Fstar.Mul, is there any need in avoiding using * as operator? It's possible to modify grammar to make it work for both tuples and multiplication, so what's the point then? People who want to use × will be allowed to use it, while people who port and verify their F#/OCaml software won't be bothered with the need to use Unicode symbols.

[msprotz]

I think the root issue is that with universes, both t₁ * t₂ and t₁ × t₂ are valid... the former is a tuple (i.e. Prims.tuple2 t₁ t₂) and the latter is a product of two terms... where t₁ and t₂ can be any two terms... how would you fix the grammar?

[msprotz]

More specifically, the parser doesn't distinguish between types and terms; there's a cascade of precedence levels, and somewhere in the cascade is tmTuple. The relevant bits are:

 603 typ:
 604   | simpleTerm  { $1 }

simpleTerm fallbacks on tmIff, then all the way to tmTuple.

If we had menhir, we could parameterize the cascade over the meaning of the * symbol, and use a different entry point for types and terms, but barring that, the duplication effort seems high. I already duplicated a bunch of stuff because of that (see tmArrowNoEquals).

[tahina-pro]

Catalin: discussion moved to separate issue (#770) about POPL release.

[A-Manning]

On the topic of z3, would that just require calling z3 with memory_max_alloc_count and rlimit flags, or is there something more elaborate needed?

[catalin-hritcu]

@A-Manning It's indeed "only" a matter of setting rlimit instead of timeout, just that currently many F* files set timeout to magic constants which we will need to convert. Tracking this in #767, so let's continue any discussions there.