From d300be95c28ff3147bb6f6a65992df5b9b571bdf Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 10 Nov 2023 18:04:29 +0100
Subject: Check in nix that the regenerated files don't differ from the checked
 out files

---
 flake.nix | 21 +++++++++++++++++++--
 1 file changed, 19 insertions(+), 2 deletions(-)

diff --git a/flake.nix b/flake.nix
index ebe1e90d..e2b7a796 100644
--- a/flake.nix
+++ b/flake.nix
@@ -92,11 +92,28 @@
             cp ${aeneas}/bin/aeneas_driver aeneas.exe
             export AENEAS_EXE=./aeneas.exe
 
-            # Run the tests
+            # 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 - remark: we could remove the file
             make tests -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
+              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"
+              exit 1
+            fi
           '';
           # Tests don't generate anything new as the generated files are
-          # versionned, but the installation phase still needs to prodocue
+          # versionned, but the installation phase still needs to produce
           # something, otherwise Nix will consider the build has failed.
           installPhase = "touch $out";
         };
-- 
cgit v1.2.3