Merge pull request #132 from AeneasVerif/regen-tests

Ensure we regenerate files properly in CI

1 files changed, 3 insertions, 6 deletions

diff --git a/flake.nix b/flake.nix
index a436d773..f6a5f04e 100644
--- a/flake.nix
+++ b/flake.nix
@@ -75,23 +75,20 @@
             export AENEAS_EXE=./aeneas
 
             # Copy the tests
-            mkdir tests-copy
             cp -r tests tests-copy
 
-            # TODO: remove the test files to make sure we regenerate exactly
-            # the files which are checked out (we have to be careful about
-            # files like lakefile.lean, and the user hand-written files)
-
             # Run the tests with extra sanity checks enabled
             # Remark: we could remove the file
+            make clean-generated
             OPTIONS=-checks make test-all -j $NIX_BUILD_CORES
 
             # Check that there are no differences between the generated tests
             # and the original tests
-            if [[ $(diff -rq tests tests-copy) ]]; then
+            if diff -rq tests tests-copy; then
               echo "Ok: the regenerated test files are the same as the checked out files"
             else
               echo "Error: the regenerated test files differ from the checked out files"
+              diff -ru tests tests-copy
               exit 1
             fi
           '';