Releases · CertiRocq/certirocq

We are happy to announce the release of CertiRocq 0.9.1 for Rocq 9.1. CertiRocq is a formally verified compiler from Gallina, the internal language of Rocq down to CompCert Clight and WebAssembly. It can be used to compile Rocq programs to WebAssembly or C programs which can be further compiled with compcert or any other C compiler. See the CertiRocq wiki for a detailed description of the project and provided plugins. This release implements renaming from CertiCoq to CertiRocq, porting to Rocq 9.1 by @4ever2 and @yforster, support for Nix (in the CI in particular), and adds a verified WebAssembly backend by @womeier et al. It also benefits from new optimization phases from MetaCoq 1.5.1. In particular, it supports a new (unverified) phase to map inductive types to arbitrary C code, through the existing support for extracting constants. An example (lightly tested!) binding of Rocq's Corelib nat to GMP arbitrary precision integers, with fast path for int63 values, à la zarith is provided.

-- The CertiRocq Team

What's Changed

Implement and verify the naive translation of lazy/force to thunks by @mattam82 in #98
Fixes in prim_int63.c by @mattam82 in #99
Verified reordering cleanup by @mattam82 in #100
Update build.yml and .opam file to use released MetaCoq 1.3.2 and cor… by @mattam82 in #101
Remove dead code by @zoep in #112
Requires OCaml 4.13 by @liyishuai in #106
opam: remove with-test commands by @SkySkimmer in #105
Support for Coq 8.20 by @yforster in #115
WebAssembly backend by @womeier in #103
Nix config by @womeier in #130
Fix typos in documentation of exp and fundefs by @tom93 in #131
docs (benchmarks/README.md): fix typo in word "benchmarking" by @gap-editor in #125
Port to Rocq 9.1 by @4ever2 in #135
Rename CertiCoq to CertiRocq by @mattam82 in #136
Port to metarocq 1.5.1 by @mattam82 in #138
Certirocq eval fixes by @mattam82 in #139
Primstring gmp bindings by @mattam82 in #141
Improve GMP bindings and prim_int63, WIP remapping of inductives by @mattam82 in #142