Summary

A lot has been going on, with more than 530 patches and 70 PRs merged since 0.7.0 last summer. Too many changes to list here in detail, so below are a few highlights, and check 0.7.0...0.8.0 for exhaustivity.

Notable caveat: installation of the Python dependencies has been reworked: make dependencies-python should set up reliably for both syntax highlighting in literal output, and running generated Python code (see french_law/python), but you will now have to either rely on the make rules, or run . _python_venv/bin/activate each time before your commands.

What's changed

• Quite a lot of syntax improvements and changes. Checkout the latest cheat-sheet for an overview

• Allow local let ... equals ... in ... definitions

• Better error messages and positions throughout

• Added the ability to directly call a scope and retrieve its outputs, like a function

• Added disambiguation, allowing to access structure fields without specifying the structure type each time

• Added automated resolution of operators, allowing e.g. to write just + in place of all the type-specific operators +., +$, +@, +^, etc.

• More consistent priority for operators. It is no longer allowed to write a and b or c without parenthesis.

• Added and changed some operators (date + duration now allowed either way, int / int now returns a decimal, added duration / duration)

• Added the ability to have variables and functions defined at top-level (outside of any scope). See annex A of the tutorial for details.

• Added support for functions with multiple arguments

• Some big refactors in the compiler, allowing much better code sharing between the different passes, and making it much easier to extend. Also added the possibility to run the type-checker earlier, etc.

• Countless bug-fixes

• Improvements to our proof backend with Z3

• A tool to automatically synchronise with the upstream French law from Legifrance