Add testing of documentation examples

Ref. eng/recordflux/RecordFlux#1501

.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:

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

doc/examples/.gitignore

@@ -1,2 +1 @@
-generated
-obj
+build

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 $@) $<

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",