From cbcaa965c4ee5597bb8f4f8bee7fba87729e7154 Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko
Date: Mon, 23 Jan 2023 18:17:42 -0800
Subject: Initial Lean backend, WIP

---
 Makefile | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 19ba0b6f..1533668c 100644
--- a/Makefile
+++ b/Makefile
@@ -186,7 +186,7 @@ gen-llbcp-%:
 .PHONY: trans-%
 trans-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR)
 trans-%: FILE = $*
-trans-%: gen-llbc-% tfstar-% tcoq-%
+trans-%: gen-llbc-% tfstar-% tcoq-% tlean-%
 	echo "# Test $* done"
 
 # "p" stands for "Polonius"
@@ -222,6 +222,12 @@ tcoqp-%: BACKEND_SUBDIR := coq
 tcoqp-%:
 	$(AENEAS_CMD)
 
+.PHONY: tlean-%
+tlean-%: OPTIONS += -backend lean -test-trans-units
+tlean-%: BACKEND_SUBDIR := lean
+tlean-%:
+	$(AENEAS_CMD)
+
 # Nix
 .PHONY: nix
 nix: nix-aeneas-tests nix-aeneas-verify-fstar nix-aeneas-verify-coq
-- 
cgit v1.2.3