Merge PR #11413: [doc] [ltac2] Build Ltac2 documentation

Reviewed-by: Zimmi48

4 files changed, 42 insertions, 8 deletions

diff --git a/Makefile.doc b/Makefile.doc
index 125a4b33d5..50c4acb416 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -129,6 +129,8 @@ doc/unreleased.rst: $(wildcard doc/changelog/00-title.rst doc/changelog/*/*.rst)
 # Standard library
 ######################################################################
 
+DOCLIBS=-R theories Coq -R plugins Coq -Q user-contrib/Ltac2 Ltac2
+
 ### Standard library (browsable html format)
 
 ifdef QUICK
@@ -139,7 +141,7 @@ endif
 	- rm -rf doc/stdlib/html
 	$(MKDIR) doc/stdlib/html
 	$(COQDOC) -q -d doc/stdlib/html --with-header doc/common/styles/html/$(HTMLSTYLE)/header.html --with-footer doc/common/styles/html/$(HTMLSTYLE)/footer.html --multi-index --html -g \
-	  -R theories Coq -R plugins Coq $(VFILES)
+	  $(DOCLIBS) $(VFILES)
 	mv doc/stdlib/html/index.html doc/stdlib/html/genindex.html
 
 doc/stdlib/index-list.html: doc/stdlib/index-list.html.template doc/stdlib/make-library-index
@@ -178,12 +180,12 @@ doc/stdlib/FullLibrary.tex: doc/stdlib/Library.tex
 ifdef QUICK
 doc/stdlib/FullLibrary.coqdoc.tex:
 	$(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \
-            -R theories Coq -R plugins Coq $(VFILES) > $@
+            $(DOCLIBS) $(VFILES) > $@
 	sed -i.tmp -e 's///g' $@ && rm $@.tmp
 else
 doc/stdlib/FullLibrary.coqdoc.tex: $(COQDOC) $(ALLVO)
 	$(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \
-            -R theories Coq -R plugins Coq $(VFILES) > $@
+            $(DOCLIBS) $(VFILES) > $@
 	sed -i.tmp -e 's///g' $@ && rm $@.tmp
 endif
 
diff --git a/doc/stdlib/dune b/doc/stdlib/dune
index 7fe2493fbf..828caecabc 100644
--- a/doc/stdlib/dune
+++ b/doc/stdlib/dune
@@ -5,7 +5,8 @@
  (deps
    make-library-index index-list.html.template hidden-files
    (source_tree %{project_root}/theories)
-   (source_tree %{project_root}/plugins))
+   (source_tree %{project_root}/plugins)
+   (source_tree %{project_root}/user-contrib))
  (action
   (chdir %{project_root}
    ; On windows run will fail
@@ -17,6 +18,7 @@
    ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg
    (source_tree %{project_root}/theories)
    (source_tree %{project_root}/plugins)
+   (source_tree %{project_root}/user-contrib)
    (:header %{project_root}/doc/common/styles/html/coqremote/header.html)
    (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html)
    ; For .glob files, should be gone when Coq Dune is smarter.
@@ -24,7 +26,7 @@
  (action
   (progn
    (run mkdir -p html)
-   (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq $(find %{project_root}/theories %{project_root}/plugins -name *.v)")
+   (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq -Q %{project_root}/user-contrib/Ltac2 Ltac2 $(find %{project_root}/theories %{project_root}/plugins %{project_root}/user-contrib -name *.v)")
    (run mv html/index.html html/genindex.html)
    (with-stdout-to
      _index.html
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index ac611926b3..5e13214a1a 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -626,6 +626,31 @@ through the <tt>Require Import</tt> command.</p>
     plugins/ssr/ssrfun.v
   </dd>
 
+  <dt> <b>Ltac2</b>:
+    The Ltac2 tactic programming language
+  </dt>
+  <dd>
+    user-contrib/Ltac2/Ltac2.v
+    user-contrib/Ltac2/Array.v
+    user-contrib/Ltac2/Bool.v
+    user-contrib/Ltac2/Char.v
+    user-contrib/Ltac2/Constr.v
+    user-contrib/Ltac2/Control.v
+    user-contrib/Ltac2/Env.v
+    user-contrib/Ltac2/Fresh.v
+    user-contrib/Ltac2/Ident.v
+    user-contrib/Ltac2/Init.v
+    user-contrib/Ltac2/Int.v
+    user-contrib/Ltac2/List.v
+    user-contrib/Ltac2/Ltac1.v
+    user-contrib/Ltac2/Message.v
+    user-contrib/Ltac2/Notations.v
+    user-contrib/Ltac2/Option.v
+    user-contrib/Ltac2/Pattern.v
+    user-contrib/Ltac2/Std.v
+    user-contrib/Ltac2/String.v
+  </dd>
+
   <dt> <b>Unicode</b>:
     Unicode-based notations
   </dt>
diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index
index bea6f24098..732f15b78a 100755
--- a/doc/stdlib/make-library-index
+++ b/doc/stdlib/make-library-index
@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/usr/bin/env bash
 
 # Instantiate links to library files in index template
 
@@ -8,9 +8,14 @@ HIDDEN=$2
 cp -f $FILE.template tmp
 echo -n "Building file index-list.prehtml... "
 
-LIBDIRS=`find theories/* plugins/* -type d ! -name .coq-native`
+LIBDIRS=`find theories/* plugins/* user-contrib/* -type d ! -name .coq-native`
 
 for k in $LIBDIRS; do
+    if [[ $k =~ "user-contrib" ]]; then
+        BASE_PREFIX=""
+    else
+        BASE_PREFIX="Coq."
+    fi
     d=`basename $k`
       ls $k | grep -q \.v'$'
       if [ $? = 0 ]; then
@@ -26,7 +31,7 @@ for k in $LIBDIRS; do
                     echo Error: $FILE and $HIDDEN both mention $k/$b.v; exit 1
                 else
 		    p=`echo $k | sed 's:^[^/]*/::' | sed 's:/:.:g'`
-		    sed -e "s:$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2
+		    sed -e "s:$k/$b.v:<a href=\"$BASE_PREFIX$p.$b.html\">$b</a>:g" tmp > tmp2
 		    mv -f tmp2 tmp
                 fi
 	    else