diff options
author | Son HO | 2024-04-19 08:24:37 +0200 |
---|---|---|
committer | GitHub | 2024-04-19 08:24:37 +0200 |
commit | ad764b07c7a576eb509e08a29868e719fe5d8a84 (patch) | |
tree | 678ae9c0edcf90925b5db65c8f2ada3d68073f9a | |
parent | caedb227fcf018a5e9e6f5627144a9bf0b5484c3 (diff) | |
parent | 04f65cb173978ac9010ae88a24e6106382669fa1 (diff) |
Merge pull request #132 from AeneasVerif/regen-tests
Ensure we regenerate files properly in CI
-rw-r--r-- | Makefile | 8 | ||||
-rw-r--r-- | flake.nix | 9 | ||||
-rw-r--r-- | tests/coq/betree/BetreeMain_FunsExternal.v | 1 | ||||
-rw-r--r-- | tests/coq/betree/BetreeMain_TypesExternal.v | 1 | ||||
-rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v | 1 | ||||
-rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v | 1 | ||||
-rw-r--r-- | tests/coq/misc/External_FunsExternal.v | 1 | ||||
-rw-r--r-- | tests/coq/misc/External_TypesExternal.v | 1 | ||||
-rw-r--r-- | tests/lean/External/Opaque.lean | 1 | ||||
-rw-r--r-- | tests/lean/HashmapMain/Opaque.lean | 1 |
10 files changed, 10 insertions, 15 deletions
@@ -83,7 +83,7 @@ doc: cd compiler && dune build @doc .PHONY: clean -clean: +clean: clean-generated cd compiler && dune clean # Test the project by translating test files to F* @@ -99,6 +99,12 @@ test-all: test-no_nested_borrows test-paper \ test-loops \ test-arrays test-traits test-bitwise test-demo +.PHONY: clean-generated +clean-generated: + # We can't put this line in `tests/Makefile` otherwise it will detect itself. + # FIXME: generation of hol4 files is deactivated so we don't delete those. + grep -lR 'THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS' tests | grep -v '^tests/hol4' | xargs rm + # Verify the F* files generated by the translation .PHONY: verify verify: @@ -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 ''; diff --git a/tests/coq/betree/BetreeMain_FunsExternal.v b/tests/coq/betree/BetreeMain_FunsExternal.v index 07dba263..2d77c4ed 100644 --- a/tests/coq/betree/BetreeMain_FunsExternal.v +++ b/tests/coq/betree/BetreeMain_FunsExternal.v @@ -1,4 +1,3 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) (** [betree_main]: external functions. -- This is a template file: rename it to "FunsExternal.lean" and fill the holes. *) Require Import Primitives. diff --git a/tests/coq/betree/BetreeMain_TypesExternal.v b/tests/coq/betree/BetreeMain_TypesExternal.v index 50c4a4f8..870d2601 100644 --- a/tests/coq/betree/BetreeMain_TypesExternal.v +++ b/tests/coq/betree/BetreeMain_TypesExternal.v @@ -1,4 +1,3 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) (** [betree_main]: external types. -- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *) Require Import Primitives. diff --git a/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v index a03dc407..fb5f23cd 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v @@ -1,4 +1,3 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) (** [hashmap_main]: external function declarations *) Require Import Primitives. Import Primitives. diff --git a/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v b/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v index 87568232..28651c14 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v @@ -1,4 +1,3 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) (** [hashmap_main]: external types. -- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *) Require Import Primitives. diff --git a/tests/coq/misc/External_FunsExternal.v b/tests/coq/misc/External_FunsExternal.v index 130b48a2..39f4a60e 100644 --- a/tests/coq/misc/External_FunsExternal.v +++ b/tests/coq/misc/External_FunsExternal.v @@ -1,4 +1,3 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) (** [external]: external function declarations *) Require Import Primitives. Import Primitives. diff --git a/tests/coq/misc/External_TypesExternal.v b/tests/coq/misc/External_TypesExternal.v index 3f02b839..734c66e5 100644 --- a/tests/coq/misc/External_TypesExternal.v +++ b/tests/coq/misc/External_TypesExternal.v @@ -1,4 +1,3 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) (** [external]: external types. -- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *) Require Import Primitives. diff --git a/tests/lean/External/Opaque.lean b/tests/lean/External/Opaque.lean index d0297523..6cec334f 100644 --- a/tests/lean/External/Opaque.lean +++ b/tests/lean/External/Opaque.lean @@ -1,4 +1,3 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS -- [external]: opaque function definitions import Base import External.Types diff --git a/tests/lean/HashmapMain/Opaque.lean b/tests/lean/HashmapMain/Opaque.lean index abf04c94..a410b253 100644 --- a/tests/lean/HashmapMain/Opaque.lean +++ b/tests/lean/HashmapMain/Opaque.lean @@ -1,4 +1,3 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS -- [hashmap_main]: opaque function definitions import Base import HashmapMain.Types |