From 87d6f6c7c90bf7b427397d6bd2e2c70d610678e3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 4 Jul 2023 14:57:51 +0200
Subject: Reorganize the Lean tests

---
 Makefile | 32 +++++++++++++-------------------
 1 file changed, 13 insertions(+), 19 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index a5d1fd09..1b11592f 100644
--- a/Makefile
+++ b/Makefile
@@ -117,8 +117,8 @@ trans-no_nested_borrows trans-paper: \
 	OPTIONS += -test-units -test-trans-units -no-split-files -no-state
 trans-no_nested_borrows trans-paper: SUBDIR := misc
 tfstar-no_nested_borrows tfstar-paper:
-tlean-no_nested_borrows: SUBDIR := misc-no_nested_borrows
-tlean-paper: SUBDIR := misc-paper
+tlean-no_nested_borrows: SUBDIR :=
+tlean-paper: SUBDIR :=
 thol4-no_nested_borrows: SUBDIR := misc-no_nested_borrows
 thol4-paper: SUBDIR := misc-paper
 
@@ -126,29 +126,29 @@ trans-loops: OPTIONS += -no-state
 trans-loops: SUBDIR := misc
 tfstar-loops: OPTIONS += -decreases-clauses -template-clauses
 tcoq-loops: OPTIONS += -use-fuel -no-split-files
-tlean-loops: SUBDIR := misc-loops
-tlean-loops: OPTIONS += -decreases-clauses -template-clauses
+tlean-loops: SUBDIR :=
 thol4-loops: SUBDIR := misc-loops
 
 trans-hashmap: OPTIONS += -no-state
 trans-hashmap: SUBDIR := hashmap
 tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses
 tcoq-hashmap: OPTIONS += -use-fuel
-tlean-hashmap: OPTIONS += -decreases-clauses -template-clauses
+tlean-hashmap: SUBDIR :=
+tlean-hashmap: OPTIONS +=
 thol4-hashmap: OPTIONS +=
 
 trans-hashmap_main: OPTIONS +=
 trans-hashmap_main: SUBDIR := hashmap_on_disk
 tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses
 tcoq-hashmap_main: OPTIONS += -use-fuel
-tlean-hashmap_main: OPTIONS += -decreases-clauses -template-clauses
+tlean-hashmap_main: SUBDIR :=
 thol4-hashmap_main: OPTIONS +=
 
 transp-polonius_list: OPTIONS += -test-units -test-trans-units -no-split-files -no-state
 transp-polonius_list: SUBDIR := misc
 tfstarp-polonius_list: OPTIONS +=
 tcoqp-polonius_list: OPTIONS +=
-tleanp-polonius_list: SUBDIR := misc-polonius_list
+tleanp-polonius_list: SUBDIR :=
 tleanp-polonius_list: OPTIONS +=
 thol4p-polonius_list: SUBDIR := misc-polonius_list
 thol4p-polonius_list: OPTIONS +=
@@ -157,7 +157,7 @@ trans-constants: OPTIONS += -test-units -test-trans-units -no-split-files -no-st
 trans-constants: SUBDIR := misc
 tfstar-constants: OPTIONS +=
 tcoq-constants: OPTIONS +=
-tlean-constants: SUBDIR := misc-constants
+tlean-constants: SUBDIR :=
 tlean-constants: OPTIONS +=
 thol4-constants: SUBDIR := misc-constants
 thol4-constants: OPTIONS +=
@@ -166,7 +166,7 @@ trans-external: OPTIONS +=
 trans-external: SUBDIR := misc
 tfstar-external: OPTIONS +=
 tcoq-external: OPTIONS +=
-tlean-external: SUBDIR := misc-external
+tlean-external: SUBDIR :=
 tlean-external: OPTIONS +=
 thol4-external: SUBDIR := misc-external
 thol4-external: OPTIONS +=
@@ -176,7 +176,8 @@ transp-betree_main: OPTIONS += -backward-no-state-update
 transp-betree_main: SUBDIR:=betree
 tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
 tcoqp-betree_main: OPTIONS += -use-fuel
-tleanp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
+tleanp-betree_main: SUBDIR :=
+tleanp-betree_main: OPTIONS +=
 thol4-betree_main: OPTIONS +=
 
 # Additional test on the betree: translate it without `-backward-no-state-update`.
@@ -249,8 +250,7 @@ tcoqp-%:
 	$(AENEAS_CMD)
 
 .PHONY: tlean-%
-# TODO: add  -test-trans-units once we remove all the sorry from Primitives.lean
-tlean-%: OPTIONS += -backend lean
+tlean-%: OPTIONS += -backend lean -test-trans-units
 tlean-%: BACKEND_SUBDIR := lean
 tlean-%:
 	$(AENEAS_CMD)
@@ -258,13 +258,7 @@ tlean-%:
 # "p" stands for "Polonius"
 .PHONY: tleanp-%
 
-# TODO: for now we don't extract the betree for Lean because we need to implement
-# proper support for the proofs of termination for the mutually recursive functions.
-tleanp-betree_main:
-	echo "Ignoring Lean betree"
-
-# TODO: add  -test-trans-units once we remove all the sorry from Primitives.lean
-tleanp-%: OPTIONS += -backend lean
+tleanp-%: OPTIONS += -backend lean -test-trans-units
 tleanp-%: BACKEND_SUBDIR := lean
 tleanp-%:
 	$(AENEAS_CMD)
-- 
cgit v1.2.3