diff options
| author | Son Ho | 2023-11-09 14:22:06 +0100 |
|---|---|---|
| committer | Son Ho | 2023-11-09 14:22:06 +0100 |
| commit | 9157959cc421c481cf584ada69f51d58da82e8f9 (patch) | |
| tree | 77ae816309919eb9d97df6d5ca63c6649af324f3 /Makefile | |
| parent | eec2643daad40d3ceec51cd83eb01e7c9db1824d (diff) | |
Deactivate the HOL4 tests
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 12 |
1 files changed, 10 insertions, 2 deletions
@@ -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 |