add support for publishing coqdoc

buildjob

@@ -15,6 +15,10 @@ set -e
 ##   non-empty, submit timing information to coq-speed with the given project
 ##   name and configuration string.  Reqires the $TIMING_SECRET variable to be
 ##   set.
+## - $DOC_DIR, $DOC_BRANCH, $DOC_KEY: If $DOC_DIR is non-empty, run coqdoc and
+##   upload the results to the given directory.  This only happens if the
+##   current branch is $DOC_BRANCH (defaults to master).  Requires the $DOC_KEY
+##   variable to be set to the secret key for uploading.
 
 # Parepare
 . ci/ansi-colors.sh
@@ -31,7 +35,7 @@ cat build-log.txt | egrep "(real|user): [0-9]" | tee build-time.txt
 # maybe validate
 if [[ -n "$VALIDATE" ]]; then
     echo_color "$BOLDGREEN" "[buildjob] Performing validation"
-    make validate;
+    make validate
 fi
 
 # maybe submit timing information
@@ -40,6 +44,7 @@ if [[ -n "$TIMING_PROJECT" && -n "$TIMING_CONF" ]]; then
     # check if we have the secret
     if [[ -z "$TIMING_SECRET" ]]; then
         echo_color "$BOLDRED" "[buildjob] TIMING_SECRET variable is missing"
+        exit 1
     fi
     # Submit to webhook endpoint
     curl --fail -sS -X POST https://coq-speed.mpi-sws.org/webhook/build_times \
@@ -52,12 +57,33 @@ if [[ -n "$TIMING_PROJECT" && -n "$TIMING_CONF" ]]; then
          --data-binary @- < build-time.txt
 fi
 
+# maybe generate and upload documentation
+if [[ -n "$DOC_DIR" && "$CI_COMMIT_REF_NAME" == "${DOC_BRANCH:-master}" ]]; then
+  echo_color "$BOLDGREEN" "Publishing documentation from branch $CI_COMMIT_REF_NAME to $DOC_DIR"
+  # check if we have the secret
+  if [[ -z "$DOC_KEY" ]]; then
+      echo_color "$BOLDRED" "[buildjob] DOC_KEY variable is missing"
+      exit 1
+  fi
+
+  # We need a custom wrapper around SSH to use our settings, and ssh-agent for the key
+  eval $(ssh-agent -s)
+  echo "${DOC_KEY}" | tr -d '\r' | ssh-add -
+  export GIT_SSH=$(readlink -e ci/ssh)
+
+  # Generate documentation
+  make html
+  # Upload documentation
+  rsync -a --delete -e "$GIT_SSH" html/ "$DOC_DIR/"
+fi
+
 # maybe create opam package
 if [[ -n "$OPAM_PKG" && "$CI_COMMIT_REF_NAME" == "${OPAM_PKG_BRANCH:-master}" ]]; then
     echo_color "$BOLDGREEN" "[buildjob] Releasing package on opam"
     # check if we have the secret
     if [[ -z "$OPAM_UPDATE_SECRET" ]]; then
         echo_color "$BOLDRED" "[buildjob] OPAM_UPDATE_SECRET variable is missing"
+        exit 1
     fi
     # determine package name prefix
     if [[ "$CI_COMMIT_REF_NAME" == master ]]; then