cakeml icon indicating copy to clipboard operation
cakeml copied to clipboard

Add code quality tests to regression

Open myreen opened this issue 1 year ago • 0 comments

At present, the compiler proofs are regression tested. This means the compiler generated code will always stay correct. However, the compiler and its configuration are not currently tested for quality.

This issue is about adding a collection of simple tests that ensure optimisations trigger in situations they are supposed to be triggered. One could, e.g., take a few simple code snippets, compile them to dataLang, and check that certain small functions are inlined in the generated dataLang program. See examples/cost for nice pretty printing of dataLang programs.

The same can be done for wordLang, one could check wordLang optimisations using functions already present in examples/compilation/to_word.

myreen avatar Jul 08 '23 14:07 myreen