From 8f4a636c8b3f462ff39bb7ce11112cd095a8b4f7 Mon Sep 17 00:00:00 2001
From: Tobias Reiher <reiher@adacore.com>
Date: Thu, 10 Aug 2023 16:12:33 +0200
Subject: [PATCH] Fix GNATprove caching

Ref. eng/recordflux/RecordFlux#1391
---
 Makefile                           | 14 +-------------
 Makefile.common                    | 15 +++++++++++++++
 examples/apps/dhcp_client/Makefile |  4 ++--
 examples/apps/ping/Makefile        |  4 ++--
 tests/spark/Makefile               |  4 ++--
 5 files changed, 22 insertions(+), 19 deletions(-)
 create mode 100644 Makefile.common

diff --git a/Makefile b/Makefile
index 6d72f6ed5..be4012b3a 100644
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,5 @@
 -include devutils/Makefile.common
+include Makefile.common
 
 .DEFAULT_GOAL := all
 
@@ -11,9 +12,7 @@ ADASAT_ORIGIN?= https://github.com/AdaCore
 VERSION ?= $(shell python3 -c "import setuptools_scm; print(setuptools_scm.get_version())")
 SDIST ?= dist/RecordFlux-$(VERSION).tar.gz
 
-BUILD_DIR = build
 GENERATED_DIR = generated
-MAKEFILE_DIR := $(dir $(abspath Makefile))
 BUILD_GENERATED_DIR := $(MAKEFILE_DIR)/$(BUILD_DIR)/$(GENERATED_DIR)
 PYTHON_PACKAGES = bin doc/language_reference/conf.py doc/user_guide/conf.py examples/apps ide language rflx tests tools stubs setup.py
 DEVUTILS_HEAD = 7f4319741b23b926aca093467e097005d4a1f642
@@ -24,14 +23,6 @@ ADASAT_HEAD = f948e2271aec51f9313fa41ff3c00230a483f9e8
 SHELL = /bin/bash
 PYTEST = python3 -m pytest -n$(TEST_PROCS) -vv --timeout=7200
 
-# Use GNATprove's file-based caching by default and ensure the directory exists.
-GNATPROVE_CACHE ?= file:$(MAKEFILE_DIR)/$(BUILD_DIR)/gnatprove_cache
-
-ifneq (,$(findstring file:,$(GNATPROVE_CACHE)))
-GNATPROVE_CACHE_DIR = $(subst file:,,$(GNATPROVE_CACHE))
-endif
-
-export GNATPROVE_CACHE := $(GNATPROVE_CACHE)
 export PYTHONPATH := $(MAKEFILE_DIR)
 
 # Switch to a specific revision of the git repository.
@@ -210,9 +201,6 @@ prove_apps: $(GNATPROVE_CACHE_DIR)
 prove_property_tests: $(GNATPROVE_CACHE_DIR)
 	$(PYTEST) tests/property_verification
 
-$(GNATPROVE_CACHE_DIR):
-	mkdir -p $(GNATPROVE_CACHE_DIR)
-
 .PHONY: install_build_deps install install_devel upgrade_devel install_devel_edge install_git_hooks install_gnat printenv_gnat
 
 install_build_deps:
diff --git a/Makefile.common b/Makefile.common
new file mode 100644
index 000000000..177b04865
--- /dev/null
+++ b/Makefile.common
@@ -0,0 +1,15 @@
+BUILD_DIR = build
+MAKEFILE_DIR := $(dir $(abspath $(lastword $(MAKEFILE_LIST))))
+GNATPROVE = $(MAKEFILE_DIR)tools/gnatprove
+
+# Use GNATprove's file-based caching by default and ensure the directory exists.
+GNATPROVE_CACHE ?= file:$(MAKEFILE_DIR)$(BUILD_DIR)/gnatprove_cache
+
+ifneq (,$(findstring file:,$(GNATPROVE_CACHE)))
+GNATPROVE_CACHE_DIR = $(subst file:,,$(GNATPROVE_CACHE))
+endif
+
+export GNATPROVE_CACHE := $(GNATPROVE_CACHE)
+
+$(GNATPROVE_CACHE_DIR):
+	mkdir -p $(GNATPROVE_CACHE_DIR)
diff --git a/examples/apps/dhcp_client/Makefile b/examples/apps/dhcp_client/Makefile
index 1c9a93efb..b5ff16412 100644
--- a/examples/apps/dhcp_client/Makefile
+++ b/examples/apps/dhcp_client/Makefile
@@ -1,4 +1,4 @@
-GNATPROVE = ../../../tools/gnatprove
+include ../../../Makefile.common
 
 specs = $(wildcard specs/*.rflx)
 src = generated/rflx-dhcp_client.ads
@@ -12,7 +12,7 @@ test: $(bin)
 
 build: $(bin)
 
-prove: $(src)
+prove: $(GNATPROVE_CACHE_DIR) $(src)
 	$(GNATPROVE) -Pdhcp_client
 
 generate: $(src)
diff --git a/examples/apps/ping/Makefile b/examples/apps/ping/Makefile
index 2170d3941..960dbe018 100644
--- a/examples/apps/ping/Makefile
+++ b/examples/apps/ping/Makefile
@@ -1,4 +1,4 @@
-GNATPROVE = ../../../tools/gnatprove
+include ../../../Makefile.common
 
 specs = $(wildcard specs/*.rflx)
 src = generated/rflx.ads
@@ -16,7 +16,7 @@ test_spark: $(bin)
 
 build: $(bin)
 
-prove: $(src)
+prove: $(GNATPROVE_CACHE_DIR) $(src)
 	$(GNATPROVE) -Pping
 
 generate: $(src)
diff --git a/tests/spark/Makefile b/tests/spark/Makefile
index 14255e8d6..348bff086 100644
--- a/tests/spark/Makefile
+++ b/tests/spark/Makefile
@@ -1,4 +1,4 @@
-GNATPROVE = ../../tools/gnatprove
+include ../../Makefile.common
 
 project := test
 ifdef TEST
@@ -28,7 +28,7 @@ test_optimized: $(test_files)
 build_strict: $(test_files)
 	gprbuild -P$(project) -Xgnat=$(GNAT) -Xmode=strict
 
-prove: $(proof_sessions) $(test_files)
+prove: $(GNATPROVE_CACHE_DIR) $(proof_sessions) $(test_files)
 	$(GNATPROVE) -P$(project) -Xtest=$(TEST)
 
 clean: