From b1661edaa3ce4c04c22cb77bdccb91b649319c9a Mon Sep 17 00:00:00 2001
From: Tobias Reiher <reiher@adacore.com>
Date: Fri, 15 Dec 2023 19:15:12 +0100
Subject: [PATCH] Ensure CLI documentation is up-to-date

Ref. eng/recordflux/RecordFlux#1491
---
 Makefile                                 |  1 +
 doc/user_guide/90-rflx--help.txt         |  2 +-
 doc/user_guide/90-rflx-install--help.txt |  5 ++--
 doc/user_guide/90-rflx-run_ls--help.txt  |  4 +++
 doc/user_guide/Makefile                  | 35 ++++++++++++++++--------
 5 files changed, 32 insertions(+), 15 deletions(-)
 create mode 100644 doc/user_guide/90-rflx-run_ls--help.txt

diff --git a/Makefile b/Makefile
index 941ea61c7..b92439646 100644
--- a/Makefile
+++ b/Makefile
@@ -118,6 +118,7 @@ check_contracts:
 
 check_doc:
 	tools/check_doc.py -d doc -x doc/user_guide/gfdl.rst
+	$(MAKE) -C doc/user_guide check_help
 
 .PHONY: test test_rflx test_examples test_coverage test_unit_coverage test_property test_tools test_ide test_optimized test_compilation test_binary_size test_installation test_specs test_apps
 
diff --git a/doc/user_guide/90-rflx--help.txt b/doc/user_guide/90-rflx--help.txt
index 7a3df47aa..dacb0562a 100644
--- a/doc/user_guide/90-rflx--help.txt
+++ b/doc/user_guide/90-rflx--help.txt
@@ -20,6 +20,6 @@ options:
   --version
   --no-verification     skip time-consuming verification of model
   --max-errors NUM      exit after at most NUM errors
-  --workers NUM         parallelize proofs among NUM workers (default: 20)
+  --workers NUM         parallelize proofs among NUM workers (default: NPROC)
   --unsafe              allow unsafe options (WARNING: may lead to erronous
                         behavior)
diff --git a/doc/user_guide/90-rflx-install--help.txt b/doc/user_guide/90-rflx-install--help.txt
index 52f9ac52c..a1fdaae93 100644
--- a/doc/user_guide/90-rflx-install--help.txt
+++ b/doc/user_guide/90-rflx-install--help.txt
@@ -1,7 +1,8 @@
-usage: rflx install [-h] [--gnat-studio-dir GNAT_STUDIO_DIR] {gnatstudio}
+usage: rflx install [-h] [--gnat-studio-dir GNAT_STUDIO_DIR]
+                    {gnatstudio,vscode}
 
 positional arguments:
-  {gnatstudio}
+  {gnatstudio,vscode}
 
 options:
   -h, --help            show this help message and exit
diff --git a/doc/user_guide/90-rflx-run_ls--help.txt b/doc/user_guide/90-rflx-run_ls--help.txt
new file mode 100644
index 000000000..4dfd1f7de
--- /dev/null
+++ b/doc/user_guide/90-rflx-run_ls--help.txt
@@ -0,0 +1,4 @@
+usage: rflx run_ls [-h]
+
+options:
+  -h, --help  show this help message and exit
diff --git a/doc/user_guide/Makefile b/doc/user_guide/Makefile
index dcd34d7af..18d30fdbb 100644
--- a/doc/user_guide/Makefile
+++ b/doc/user_guide/Makefile
@@ -7,28 +7,39 @@ BUILDDIR      = build
 help:
 	@$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
 
-.PHONY: help regenerate_help Makefile
+.PHONY: help check_help regenerate_help clean_help Makefile
 
 %: Makefile
 	@$(SPHINXBUILD) -M $@ "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
 
-HELP_FILES = \
-   90-rflx--help.txt \
-   90-rflx-check--help.txt \
-   90-rflx-generate--help.txt \
-   90-rflx-graph--help.txt \
-   90-rflx-validate--help.txt \
-   90-rflx-install--help.txt \
-   90-rflx-convert--help.txt \
-   90-rflx-run_ls--help.txt
+SHELL = /bin/bash
+COMMANDS = $(shell rflx |& sed -n 's/.*{\(.*\)}.*/\1/p' | tr ',' ' ')
+
+help_file = 90-rflx-$(1)--help.txt
+
+EXPECTED_HELP_FILES = 90-rflx--help.txt $(foreach CMD,$(COMMANDS),$(call help_file,$(CMD)))
+EXISTING_HELP_FILES = $(wildcard 90-rflx-*-help.txt)
+UNEXPECTED_HELP_FILES = $(filter-out $(EXPECTED_HELP_FILES),$(EXISTING_HELP_FILES))
+MISSING_HELP_FILES = $(filter-out $(EXISTING_HELP_FILES),$(EXPECTED_HELP_FILES))
+
+REPLACE_WORKERS = sed "s/workers (default: [0-9]*)/workers (default: NPROC)/"
+CHECK = diff 90-rflx--help.txt <(rflx --help | $(REPLACE_WORKERS)) && $(foreach CMD,$(COMMANDS),diff $(call help_file,$(CMD)) <(rflx $(CMD) --help) &&) exit
+
+check_help:
+	@test -z "$(MISSING_HELP_FILES)" || ( echo "Missing help files: $(MISSING_HELP_FILES)" && exit 1 )
+	@test -z "$(UNEXPECTED_HELP_FILES)" || ( echo "Unexpected help files: $(UNEXPECTED_HELP_FILES)" && exit 1 )
+	@( $(CHECK) ) || ( echo "Help texts are outdated" && exit 1 )
 
 90-rflx-%--help.txt::
 	@rflx $* --help > $@
 
 90-rflx--help.txt:
-	@rflx --help > $@
+	@rflx --help | $(REPLACE_WORKERS) > $@
 
 # Regenerate rflx help texts for the documentation
 # We do not do this automatically. The results are checked in as we don't
 # have rflx available during documentation creation.
-regenerate_help:: $(HELP_FILES)
+regenerate_help:: clean_help $(EXPECTED_HELP_FILES)
+
+clean_help:
+	@rm -f 90-rflx-*-help.txt