From cfda3a990cb3b24d91ce5bf8d1ddec7b265beca5 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 16 Apr 2024 13:30:03 +0200
Subject: Ensure we regenerate files properly in CI

Files that weren't regenerated were marked as not
automatically-generated.
---
 flake.nix | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

(limited to 'flake.nix')

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
           '';
-- 
cgit v1.2.3