More robust command in `Makefile.common` to generate the documentation

[affeldt-aist]

To generate the documentation for version 1.13.0 with rocqnavi, I used the following command:

machtml: build $(DOCDIR)/dependency_graph.dot
        coqdep -f _CoqProject > depend.d
        cat -n depend.d >&2
        gsed -i 's/Classical/mathcomp\.classical/' depend.d
        gsed -i 's/Theories/mathcomp\.analysis/' depend.d
        gsed -i 's/Reals_stdlib/mathcomp\.reals_stdlib/' depend.d
        gsed -i 's/Experimental_reals/mathcomp\.experimental_reals/' depend.d
        gsed -i 's/Reals/mathcomp\.reals/' depend.d
        gsed -i 's/Analysis_stdlib/mathcomp\.analysis_stdlib/' depend.d
        gsed -i 's/\//\./g' depend.d
        ~/git/coq2html/tools/generate-hierarchy-graph.sh
        rm test_interval_inference.glob
        find . -not -path '*/.*' -name "*.v" -or -name "*.glob" | xargs ~/git/coq2html/rocqnavi \
        -title "Mathcomp Analysis" \
        -d $(DOCDIR) -base mathcomp -Q theories analysis \
        -external https://rocq-prover.org/doc/V9.0.0/corelib Corelib \
        -hierarchy-graph "hierarchy-graph.dot" \
        -dependency-graph $(DOCDIR)/dependency_graph.dot \
        -external https://math-comp.github.io/htmldoc_2_3_0/ mathcomp.ssreflect \
        -external https://math-comp.github.io/htmldoc_2_3_0/ mathcomp.algebra \
        -index-blacklist ~/git/coq2html/tools/index-blacklist \
        -show-type-infomation-using-coqtop-process

It is slightly different from the one that is currently in Makefile.common which also has an html target whose status is unclear.

I think that a single, more robust command (that also works in a Linux environment) is desirable. @yoshihiro503

[yoshihiro503]

The make html command is still available and is constantly checked by CI to ensure that it is valid in the latest master branch and pull requests.
https://github.com/math-comp/analysis/actions/runs/17046036228/job/48321988320