summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-11-10 18:04:29 +0100
committerSon Ho2023-11-10 18:04:29 +0100
commitd300be95c28ff3147bb6f6a65992df5b9b571bdf (patch)
treef29805e5426f9f3fabe12d3fdadda96a1e987880
parentd527795cb5c24892617bd5f7df75450e50069194 (diff)
Check in nix that the regenerated files don't differ from the checked out files
-rw-r--r--flake.nix21
1 files 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";
};