v2021.07.17

Release v2021.07.17

v2021.06.26

Release v2021.06.26

v2021.06.23

Release v2021.06.23

v2021.06.06

Release v2021.06.06

v2021.05.28

Release v2021.05.28

This release was automatically generated, cf. PR #2275

v0.9.7.0-alpha1 (Summer Schools)

A preview for an upcoming major release in preparation for several summer schools. Precise release notes coming up in the non-alpha release, but you can already have a look at:
https://github.com/FStarLang/FStar/blob/v0.9.7.0-alpha1/CHANGES.md

v0.9.6.0

A large number of people contributed to this release: thanks to all!

Here are a few highlights:

Main new features

• Meta-F*: A metaprogramming and tactic framework, as described in this report. Code samples are in examples/tactics, examples/native_tactics and the FStar.Tactics and FStar.Reflection libraries. Many people contributed a lot to this work, especially Guido Martinez.

• Improved type inference with two-phase typechecking: We now build verification conditions for a program after a first phase of type inference. This improves inference of implicit arguments and reduces our trust in the type inference. Thanks to Aseem Rastogi!

• Caching typechecked modules: F* emits ".checked" files, an on-disk representation of a typechecked module that can be read back later. This significantly reduces the time to load a module's dependences.

Many other improvements

A sampling of improvements across the entire tool chain:

• Resolving several syntactic ambiguities in the parser

• A correct pretty printer for surface terms, using fstar --indent

• A new dependence analysis to support incremental compilation for larger projects

• Overhauling the higher order unification algorithm, both in the representation of meta-variables and in the handling of unfolding, leading to significant performance and robustness improvements (see https://github.com/FStarLang/FStar/wiki/Design-note:-Revising-the-unifier)

• Automatic generation of interfaces for modules and tighter enforcement of abstraction boundaries (see https://github.com/FStarLang/FStar/wiki/Revised-checking-of-a-module's-interface)

• Improvements to the SMT encoding, removing axioms that lead to performance problems and reducing brittleness related to optimizations in the encoding, notably shallow vs deep encodings

• Improved type-based erasure for extraction

• Several new and improved libraries, including a revised treatment of footprints for Low* programs, in FStar.Modifies

• And work by many people in Project Everest whose use of F* drove a lot of the work in this release.

• Plus many other improvements and changes as described in https://github.com/FStarLang/FStar/blob/v0.9.6.0/CHANGES.md

• And 180 closed github issues

v0.9.6.0-alpha1 (EPIT and SSFT)

A preview for an upcoming major release in preparation for several courses and tutorials.

This brings lots of improvements:

• two-phase type checking (towards disentangling type checking from checking of verification conditions), more robust wrt. inference of implicit arguments
• extraction to OCaml preserves the structure of let-bindings
• extraction now erases all pure unit functions, lemmas and ghost functions
• and many many more, see https://github.com/FStarLang/FStar/blob/v0.9.6.0-alpha1/CHANGES.md for more details.

v0.9.5.0

This is another big release with lots of changes and new features compared to v0.9.4.0

Main new features

• Proofs by reification (see this paper)
• A revision of the libraries based on a new formal account of monotonic state (see this paper)
• Extraction of programs with user-defined effects
• Experimental support for tactics
• New IDE protocol and new IDE features: autocompletion, evaluation, real-time syntax checking, jump-to-definition, type-at-point, etc.

Changes and other improvements

• A reorganization of the library and a single fstarlib.cmxa against which to link all F* programs compiled to OCaml (this change is incompatible with previous versions of F*)
• A new printer of source terms
• Revised error reporting from failed SMT queries
• Improved support for separate compilation via a binary format for checked modules
• Fixed a ton of bugs (179 closed GitHub issues)

v0.9.4.0 (Universes, DM4F)

This is a big release with lots of important changes compared to v0.9.2.0 exactly a year ago:

• Predicative hierarchy of universes with universe polymorphism
• Uniform syntax between expressions and types allowing rich type-level computation
• Dijkstra Monads for Free (https://www.fstar-lang.org/papers/dm4free/)
• Extraction to C via KreMLin (https://github.com/FStarLang/kremlin)
• New parser based on Menhir
• New pretty printer for surface syntax and fstar --indent
• Changed default effect to Tot
• Strict positivity check for inductives
• New synatax for inductive type projectors and discriminators
• Better semantics for module open and support for local opens
• Better dependency analysis
• Better error locations for Z3 failures
• Replaced Z3 timeouts with machine independent resource limits
• Cleaned up libraries and examples (a bit)
• Improvements to interactive mode
• Docker builds
• Fixed a ton of bugs (262 closed GitHub issues)