Q*cert v2.2.0

Backend

• Includes a new experimental WebAssembly (WASM) backend [Contribution by @pkel]

Build

• Fixes for portability: Q*cert now compiles and is tested on Coq 8.11 through 8.15
• Now uses Separate Extraction to OCaml code

Q*cert v2.1.1

This is a minor release with some code quality changes:

1. Rename some of the JavaScript runtime operations (getLeft and getRight)
2. Remove some lingering admits from the code

Q*cert v2.1.0

✨ This is a release of the Q*cert compiler framework for OCaml >= 4.09 and Coq >= 8.11. Also switches floating point numbers support from flocq to native Coq floats.

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

Q*cert 1.4.1

🐛 This is a bug-fix release, which adjusts the JavaScript and Java runtime so that record concatenation conforms to the specification (#118).

👩‍🔬 This release also includes a generalized inference-with-subtyping rule for record concatenation, and a more general lemma showing that record concatenation prioritizes duplicate fields on the right operand.

Q*cert 1.4.0

Compiler

• Complete correctness proof for translation between NNRSImp to ImpQcert

Operators

• new string-join operator
• toString semantic (dataToString) is now a parameter of the compiler. Old semantics remains as defaultDataToString
• Bug fixes to implementation of toString in the Java and JavaScript runtimes

Build

• Fixes to build process so tests failure gets reported by CircleCI

Q*cert 1.3.0

• Support for Coq 8.8.2 and OCaml 4.07.1
• Additional work on JavaScript backend
• Additions to built-in operators
• Bug fixes (Wrong order in bag difference)

Q*cert 1.2.0

• Support for Coq 8.8.1
• New JavaScript backend: more of the compilation pipeline is proven correct using imperative intermediate representations ; Lower level optimizations
• Bug fixes (Wrong type for float comparisons in infer with sub typing; Wrong error message when creating brand model)

Q*cert v1.1.0 with Coq 8.8.0 support

(fix) CircleCI: update opam

v1.0.9

Bug fix release