3.5.0

Administrative changes

• The binary builds are now built with GHC 9.6 rather than 9.4.

Language changes

• User-defined newtype and enum types can now derive instances for standard constraints like Eq and Cmp. This means you can use standard operations like == with your custom types. See the manual section for more information.
• The built-in types Option and Result now have derived instances for Eq, Cmp, and SignedCmp.
• We can now infer that a = Bit, from the constraint Integral [n][a].

Bug fixes

• Fix incorrect defaulting during type inference. (#1957)

• Make comparison operators lazy so that they do not evaluate any more of the data structure than is required to determine the comparison result, matching the behavior of the reference evaluator. (#1925)

• Modify project loading to update the cache after each module is validated, and make saving the cache atomic on file systems where renaming a file to an existing file is atomic. This is useful because we get partial results if the validation process is interrupted.

• Change the default behavior of -p/--project. The new behavior is that it will check all files that have changed, and also files that have not been previously verified. The old behavior would only validate files that have changed since last time.

• Add a new flag, --modified-project which gives us the old -p behavior (i.e., check only files that have changed).

• Replace the --untested-project flag with the --unsuccessful-project flag. This will run validation on all files that have not been successfully validated, including ones that perviously failed, and have not changed.

• Allow user to specify how many satisfying results satProve (from IR/Prove.hs) produces