diff options
| author | Son HO | 2024-03-08 16:51:40 +0100 |
|---|---|---|
| committer | GitHub | 2024-03-08 16:51:40 +0100 |
| commit | 169d011cbfa83d853d0148bbf6b946e6ccbe4c4c (patch) | |
| tree | ed8953634d14313d5b7d6ad204343d64eb990baf /Makefile | |
| parent | b604bb9935007a1f0e9c7f556f8196f0e14c85ce (diff) | |
| parent | 873deb005b394aca3090497e6c21ab9f8c2676be (diff) | |
Merge pull request #83 from AeneasVerif/son/backs
Remove the option to split the forward/backward functions
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 25 |
1 files changed, 4 insertions, 21 deletions
@@ -70,11 +70,9 @@ build-bin-dir: build-bin build-lib mkdir -p bin cp -f compiler/_build/default/main.exe bin/aeneas cp -f compiler/_build/default/main.exe bin/aeneas.cmxs - mkdir -p bin/backends/fstar/split - mkdir -p bin/backends/fstar/merge + mkdir -p bin/backends/fstar mkdir -p bin/backends/coq - cp -rf backends/fstar/split/*.fst* bin/backends/fstar/split/ - cp -rf backends/fstar/merge/*.fst* bin/backends/fstar/merge/ + cp -rf backends/fstar/*.fst* bin/backends/fstar/ cp -rf backends/coq/*.v bin/backends/coq/ .PHONY: doc @@ -263,29 +261,14 @@ testp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-% .PHONY: tfstar-% tfstar-%: OPTIONS += -backend fstar tfstar-%: BACKEND_SUBDIR := fstar -tfstar-%: tsplit-fstar-% +tfstar-%: $(AENEAS_CMD) # "p" stands for "Polonius" .PHONY: tfstarp-% tfstarp-%: OPTIONS += -backend fstar tfstarp-%: BACKEND_SUBDIR := fstar -tfstarp-%: tsplit-fstarp-% - $(AENEAS_CMD) - -# Test where we split the forward/backward functions -.PHONY: tsplit-fstar-% -tsplit-fstar-%: OPTIONS += -backend fstar -split-fwd-back -tsplit-fstar-%: BACKEND_SUBDIR := fstar-split -tsplit-fstar-%: - $(AENEAS_CMD) - -# Test where we split the forward/backward functions -# "p" stands for "Polonius" -.PHONY: tsplit-fstarp-% -tsplit-fstarp-%: OPTIONS += -backend fstar -split-fwd-back -tsplit-fstarp-%: BACKEND_SUBDIR := fstar-split -tsplit-fstarp-%: +tfstarp-%: $(AENEAS_CMD) .PHONY: tcoq-% |