From 455ba366f9c8d07a1f1848ec0960b1f2d161e7cf Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 22 Dec 2023 18:47:50 +0100
Subject: Update the library for F*

---
 Makefile | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 2cce30d9..37408554 100644
--- a/Makefile
+++ b/Makefile
@@ -70,9 +70,11 @@ 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
+	mkdir -p bin/backends/fstar/split
+	mkdir -p bin/backends/fstar/merge
 	mkdir -p bin/backends/coq
-	cp -rf backends/fstar/*.fst* bin/backends/fstar/
+	cp -rf backends/fstar/split/*.fst* bin/backends/fstar/split/
+	cp -rf backends/fstar/merge/*.fst* bin/backends/fstar/merge/
 	cp -rf backends/coq/*.v bin/backends/coq/
 
 .PHONY: doc
-- 
cgit v1.2.3


From 3688596f27a1ba461f48e88446b8812ec73f1a2f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 22 Dec 2023 19:09:16 +0100
Subject: Add an option to split the fwd/back functions and fix a minor issue

---
 Makefile | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 37408554..3ea8cda3 100644
--- a/Makefile
+++ b/Makefile
@@ -256,14 +256,29 @@ testp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-%
 .PHONY: tfstar-%
 tfstar-%: OPTIONS += -backend fstar
 tfstar-%: BACKEND_SUBDIR := fstar
-tfstar-%:
+tfstar-%: tsplit-fstar-%
 	$(AENEAS_CMD)
 
 # "p" stands for "Polonius"
 .PHONY: tfstarp-%
 tfstarp-%: OPTIONS += -backend fstar
 tfstarp-%: BACKEND_SUBDIR := fstar
-tfstarp-%:
+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-%:
 	$(AENEAS_CMD)
 
 .PHONY: tcoq-%
-- 
cgit v1.2.3


From 63ccbd914d5d44aa30dee38a6fcc019310ab640b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 23 Dec 2023 01:31:14 +0100
Subject: Update the Makefile

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

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 3ea8cda3..8d49a200 100644
--- a/Makefile
+++ b/Makefile
@@ -330,7 +330,8 @@ thol4p-%:
 
 # Nix - TODO: add the lean tests
 .PHONY: nix
-nix: nix-aeneas-tests nix-aeneas-verify-fstar nix-aeneas-verify-coq nix-aeneas-verify-hol4
+nix:
+	nix build && nix flake check
 
 .PHONY: nix-aeneas-tests
 nix-aeneas-tests:
@@ -340,6 +341,10 @@ nix-aeneas-tests:
 nix-aeneas-verify-fstar:
 	nix build .#checks.x86_64-linux.aeneas-verify-fstar --show-trace -L
 
+.PHONY: nix-aeneas-verify-fstar-split
+nix-aeneas-verify-fstar-split:
+	nix build .#checks.x86_64-linux.aeneas-verify-fstar-split --show-trace -L
+
 .PHONY: nix-aeneas-verify-coq
 nix-aeneas-verify-coq:
 	nix build .#checks.x86_64-linux.aeneas-verify-coq --show-trace -L
-- 
cgit v1.2.3