This marks the first official release of KreMLin, which goes along with F*'s 0.9.6.0 release. KreMLin releases and branches are now synchronized with F*.
Head out to https://fstarlang.github.io/lowstar/html/ for the work-in-progress KreMLin tutorial!
Notable improvements over the last six months:
- complete support for whole-program, mutually-recursive, parameterized data types monomorphization, including compilation of recursive equality predicates
- numerous code quality improvements, including a syntactic analysis to substantially reduce then number of
uu_variables introduced by F*'s extraction - many improvements to the visibility analysis, including the ability to hide type definitions within a .c file when they are not needed for the .h file
- restructing of kremlib to make it easy for clients to only use the minimum amount of exernal headers
See https://github.com/FStarLang/kremlin/blob/v0.9.6%2B/Changes.md for a complete list.