From 4078f2569b362920a648622be73761cddde8a288 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 9 May 2023 10:37:49 +0200
Subject: Make more updates for the Lean backend

---
 Makefile | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index c6fb7b46..26daadac 100644
--- a/Makefile
+++ b/Makefile
@@ -237,18 +237,29 @@ tcoqp-%:
 	$(AENEAS_CMD)
 
 .PHONY: tlean-%
-tlean-%: OPTIONS += -backend lean -test-trans-units
+# TODO: add  -test-trans-units once we remove all the sorry from Primitives.lean
+tlean-%: OPTIONS += -backend lean
 tlean-%: BACKEND_SUBDIR := lean
 tlean-%:
 	$(AENEAS_CMD)
 
+
+
 # "p" stands for "Polonius"
 .PHONY: tleanp-%
-tleanp-%: OPTIONS += -backend lean -test-trans-units
+
+# 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-%: BACKEND_SUBDIR := lean
 tleanp-%:
 	$(AENEAS_CMD)
 
+
 # Nix
 .PHONY: nix
 nix: nix-aeneas-tests nix-aeneas-verify-fstar nix-aeneas-verify-coq
-- 
cgit v1.2.3