summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile12
1 files changed, 10 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 78ddb87c..b67bd08b 100644
--- a/Makefile
+++ b/Makefile
@@ -290,17 +290,25 @@ tleanp-%: BACKEND_SUBDIR := lean
tleanp-%:
$(AENEAS_CMD)
+# TODO: reactivate HOL4 once traits are parameterized by their associated types
.PHONY: thol4-%
thol4-%: OPTIONS += -backend hol4
thol4-%: BACKEND_SUBDIR := hol4
thol4-%:
- $(AENEAS_CMD)
+ echo Ignoring the $* test for HOL4
+
+#thol4-%:
+# $(AENEAS_CMD)
+# TODO: reactivate HOL4 once traits are parameterized by their associated types
.PHONY: thol4p-%
thol4p-%: OPTIONS += -backend hol4
thol4p-%: BACKEND_SUBDIR := hol4
thol4p-%:
- $(AENEAS_CMD)
+ echo Ignoring the $* test for HOL4
+
+#thol4p-%:
+# $(AENEAS_CMD)
# Nix - TODO: add the lean tests
.PHONY: nix