Recent backward incompatible changes

A list of recent changes that break backward compatibility

Please list any other breaking changes you notice here

• 17/01/09 breaking change for the interactive mode: F* no longer accepts --fsi and now demands that the path to the file currently edited be passed as an argument to F* -- see https://github.com/FStarLang/fstar-mode.el/pull/41 for a sample diff for the emacs mode

• 17/01/09 changes in the semantics of what gets extracted; see What is verified, what is extracted? for the new semantics and use --extract_all to get the old semantics.

• The parser was rewritten using Menhir, which did introduce some changes: https://github.com/FStarLang/FStar/wiki/Moving-to-menhir

• Pull request #772 introduces the following non-backward-compatible syntax changes:

  • Modul (term) now becomes Modul.(term)
  • Datacon.param now becomes Datacon?.param (e.g. Some.v now becomes Some?.v)
  • Effect.action now becomes Effect?.action, similarly (and the same for reflect, etc.)
  • is_Datacon now becomes Datacon? (e.g. is_Some now becomes Some?)
  • Scopes are now honored in a more intuitive way: for instance, local opens and local definitions can be interleaved and shadow accordingly.

  As a consequence of these changes, Namespace.ident can now always be understood as ident belonging to module Namespace (i.e. Namespace is always a valid module name, not a data constructor or effect name) (except for module names or namespaces themselves)

• Backward-incompatible changes introduced by the new parser :

  • (| t |) is no longer accepted as a variant of ( t ) in particular the correct syntax for defining a dependent pair type is (x:a & b(x)) (if the parens are necessary)
  • The focusing let has been slightly modified : let ~> rec bidule = ... has been replaced by let rec ~> bidule = ...
  • The stratified specific = qualifier is not available anymore on binders i.e. the deprecated fun (=x:t) -> ... must be changed to fun ($x:t) -> ...

• ulib/ml/hyperheap has been removed in favour of a unified implementation of FStar_ST.ml in ulib/ml. Targets which use make -C ulib/ml hyperheap will break. Use make -C ulib/ml and ulib/ml/fstarlib.cmxa instead of ulib/ml/fstarlib-hyperheap.cmxa.

• The assumed Prims.qintro and Prims.ghost_lemma have been removed. Use instead the lemmas FStar.Classical.forall_intro and FStar.Classical.ghost_lemma, respectively, based on FStar.Squash.

• The command-line flag --universes has been removed; type checking using universes is now the default behavior. Use --stratified to switch to the stratified type checker (but beware that it will be soon deprecated).