Skip to content

Releases: FStarLang/karamel

First official release of KreMLin

17 May 20:46
Compare
Choose a tag to compare

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.