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)