Q*cert v2.0.0

This is a major new release of the Q*cert compiler framework. It includes a full redesign of the backend pipeline, with several new intermediate representation closer to the imperative code that is being generated. The code organization and build process have been completely overhauled.

Breaking

• Q*cert no longer targets ES5 but generates ES6 code instead (for its let variable scoping capabilities)
• The Spark Map-Reduce compilation target (formerly spark_rdd) is no longer supported

Main Changes

• New Imp imperative intermediate representation with new verified compilation path from NNRC to Imp
• New JavaScript backend based on Imp with a semi-persistent runtime

Code Organization

The code has been reorganised as follows:

./compiler -- the compiler
./compiler/core -- the main source code in Coq for the compiler
./compiler/parsing -- the various parsers
./compiler/lib -- OCaml support code
./cli -- the command lines (for OCaml, Java and Node.js)
./runtimes -- the runtimes for various backends (JavaScript / Java / Spark)

Build

• OCaml part of the build has been switched from ocamlbuild to dune
• Proper build for opam which, in addition to the Coq development, now includes the OCaml support libraries and the qcert command line