Skip to content

Commit

Permalink
Ensure CLI documentation is up-to-date
Browse files Browse the repository at this point in the history
Ref. eng/recordflux/RecordFlux#1491
  • Loading branch information
treiher committed Dec 19, 2023
1 parent d6d813e commit b1661ed
Show file tree
Hide file tree
Showing 5 changed files with 32 additions and 15 deletions.
1 change: 1 addition & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion doc/user_guide/90-rflx--help.txt
Original file line number Diff line number Diff line change
Expand Up @@ -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)
5 changes: 3 additions & 2 deletions doc/user_guide/90-rflx-install--help.txt
Original file line number Diff line number Diff line change
@@ -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
Expand Down
4 changes: 4 additions & 0 deletions doc/user_guide/90-rflx-run_ls--help.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
usage: rflx run_ls [-h]

options:
-h, --help show this help message and exit
35 changes: 23 additions & 12 deletions doc/user_guide/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit b1661ed

Please sign in to comment.