From 43bf604fb0b1f5a632b1a51371e183c2b203a8dd Mon Sep 17 00:00:00 2001
From: Tobias Reiher <reiher@adacore.com>
Date: Fri, 9 Feb 2024 15:20:27 +0100
Subject: [PATCH] Add testing of documentation examples

Ref. eng/recordflux/RecordFlux#1501
---
 .gitlab-ci.yml           | 19 +++++++++++++++++++
 Makefile                 |  7 ++++++-
 doc/examples/.gitignore  |  3 +--
 doc/examples/Makefile    | 20 ++++++++++++++++++--
 doc/examples/pub_sub.gpr |  8 ++++----
 5 files changed, 48 insertions(+), 9 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index bbca98d80..b92e05181 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -407,6 +407,25 @@ verification_apps:
     unprotect: true
     when: always
 
+verification_documentation:
+  extends: .testing
+  services:
+     - image:recordflux
+     - cpu:8
+     - mem:16
+  script:
+    - *setup_spark
+    - *setup_python
+    - make prove_doc
+  cache:
+    key: verification_documentation-$CI_COMMIT_REF_SLUG
+    paths:
+      - build/gnatprove_cache
+    fallback_keys:
+      - verification_documentation-main
+    unprotect: true
+    when: always
+
 html_documentation:
   extends: .testing
   services:
diff --git a/Makefile b/Makefile
index 5edd3b451..5f0dcf123 100644
--- a/Makefile
+++ b/Makefile
@@ -187,6 +187,7 @@ test_compilation:
 	$(MAKE) -C tests/spark test NOPREFIX=1
 	$(MAKE) -C tests/spark clean
 	$(MAKE) -C tests/spark test_optimized
+	$(MAKE) -C doc/examples build
 
 test_binary_size:
 	$(MAKE) -C examples/apps/dhcp_client test_binary_size
@@ -212,7 +213,7 @@ fuzz_parser:
 
 .PHONY: prove prove_tests prove_python_tests prove_apps prove_property_tests
 
-prove: prove_tests prove_python_tests prove_apps
+prove: prove_tests prove_python_tests prove_apps prove_doc
 
 prove_tests: $(GNATPROVE_CACHE_DIR)
 	$(MAKE) -C tests/spark prove
@@ -224,6 +225,9 @@ prove_python_tests: $(GNATPROVE_CACHE_DIR)
 prove_apps: $(GNATPROVE_CACHE_DIR)
 	$(foreach app,$(APPS),$(MAKE) -C examples/apps/$(app) prove || exit;)
 
+prove_doc:
+	$(MAKE) -C doc/examples prove
+
 prove_property_tests: $(GNATPROVE_CACHE_DIR)
 	$(PYTEST) tests/property_verification
 
@@ -366,6 +370,7 @@ clean:
 	$(MAKE) -C examples/apps/spdm_responder clean
 	$(MAKE) -C examples/apps/dccp clean
 	$(MAKE) -C rflx/ide/vscode clean
+	$(MAKE) -C doc/examples clean
 
 clean_all:
 	$(MAKE) clean
diff --git a/doc/examples/.gitignore b/doc/examples/.gitignore
index 883be5b8c..378eac25d 100644
--- a/doc/examples/.gitignore
+++ b/doc/examples/.gitignore
@@ -1,2 +1 @@
-generated
-obj
+build
diff --git a/doc/examples/Makefile b/doc/examples/Makefile
index 4ebb2c03a..37b04f528 100644
--- a/doc/examples/Makefile
+++ b/doc/examples/Makefile
@@ -1,6 +1,22 @@
-out/gnatprove/gnatprove.out: pub_sub.gpr generated/rflx.ads src/main.adb
+PROJECT_FILE = pub_sub.gpr
+SPECS = $(wildcard specs/*.rflx)
+GENERATED = build/generated/rflx.ads $(wildcard build/generated/*.{adb,ads})
+SRC = $(wildcard src/*.{adb,ads})
+BIN = build/obj/main
+
+.PHONY: build prove clean
+
+build: $(BIN)
+
+prove: $(PROJECT_FILE) $(GENERATED) $(SRC)
 	@gnatprove -P $<
 
-generated/rflx.ads: specs/pub_sub.rflx
+clean:
+	@rm -rf build
+
+$(BIN): $(PROJECT_FILE) $(GENERATED) $(SRC)
+	@gprbuild -P $<
+
+$(GENERATED): $(SPECS)
 	@mkdir -p $(dir $@)
 	@rflx generate -d $(dir $@) $<
diff --git a/doc/examples/pub_sub.gpr b/doc/examples/pub_sub.gpr
index f97fe7bf9..febf077ef 100644
--- a/doc/examples/pub_sub.gpr
+++ b/doc/examples/pub_sub.gpr
@@ -1,16 +1,16 @@
 project Pub_Sub is
    for Languages use ("Ada", "RecordFlux");
-   for Source_Dirs use ("src", "generated", "specs");
-   for Object_Dir use "obj";
+   for Source_Dirs use ("src", "build/generated", "specs");
+   for Object_Dir use "build/obj";
    for Create_Missing_Dirs use "True";
 
    package Recordflux is
-      for Output_Dir use "generated";
+      for Output_Dir use "build/generated";
    end Recordflux;
 
    package Prove is
       for Proof_Switches ("Ada") use (
-         "-j32",
+         "-j0",
          "--output=oneline",
          "--prover=z3,cvc5,altergo,colibri",
          "--steps=0",