Ergo v0.22.0-alpha.1

Introduction

This is a pre-release of Ergo 0.22

Ergo 0.22 is a major release of the compiler, with a completely re-designed code-generation pipeline leveraging improvements from the new version of Q*cert.

Changes

Build

• Upgrade from OCaml 4.07 to OCaml 4.11
• Upgrade from Coq 8.8 to Coq 8.12
• Switch from ocamlbuild to dune build system

Compiler

• Switch backend from Q*cert 1.4 to Q*cert 2.1 (See release notes here: https://github.com/querycert/qcert/releases)
• Redesign of compiler architecture
• Proof of correctness for Ergo calculus to Q*cert initial IL
• Complete code refactor

Runtime

• Migrate to Concerto 1.0
• Migrate JavaScript runtime from moment to dayjs

API

• Additional utcOffset parameter can be passed to Ergo engine

Tech notes:

• BREAKING The Ergo compiler no longer generates ES5, but ES6 (notably the generated code uses let)
• New compiler includes several additional ILs on the backend side, notably generates code using the Imp imperative intermediate language