From a47e2f6587e3507a12d4d86b9769b93e01023350 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 17 Jan 2020 01:25:06 +0100
Subject: [doc] [dune] [ltac2] Build Ltac2 documentation [dune build system]

This partially fixes #10139 ; we now build the Ltac2 documentation and
deploy it.

The fix here can be used for inspiration to do the make-based part.
---
 doc/stdlib/dune                     |  6 ++++--
 doc/stdlib/index-list.html.template | 25 +++++++++++++++++++++++++
 doc/stdlib/make-library-index       | 11 ++++++++---
 3 files changed, 37 insertions(+), 5 deletions(-)

(limited to 'doc/stdlib')

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
-- 
cgit v1.2.3