From 49280cda2946934980911a54b1cf9de31746e7f1 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Thu, 25 Jan 2018 15:46:16 +0100 Subject: [PATCH] CI: prepare for generating and uploading docs --- .gitlab-ci.yml | 3 +++ build/coqdoc | 14 ++++++++++++++ build/ssh | 3 +++ 3 files changed, 20 insertions(+) create mode 100755 build/coqdoc create mode 100755 build/ssh diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 125adad2..22bcb57e 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -20,6 +20,8 @@ variables: - 'time make -k -j$CPU_CORES TIMED=y 2>&1 | tee build-log.txt' - 'if fgrep Axiom build-log.txt >/dev/null; then exit 1; fi' - 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \((real|user): [0-9]" | tee build-time.txt' + # maybe generate and upload doc (has to be in this job as we need the .vo files) + - 'if test -n "$DOCDIR"; then build/coqdoc; fi' cache: key: "$CI_JOB_NAME" paths: @@ -52,6 +54,7 @@ build-coq.8.7.1: <<: *template variables: OPAM_PINS: "coq version 8.7.1" + DOCDIR: "center.mpi-sws.org:/www/sws-websites/plv.mpi-sws.org/iris/stdpp-doc" except: - triggers diff --git a/build/coqdoc b/build/coqdoc new file mode 100755 index 00000000..10562a0c --- /dev/null +++ b/build/coqdoc @@ -0,0 +1,14 @@ +#!/bin/bash +# Script to automatically generate and publish coqdoc via CI. +# This reads the following environment variables: +# - DOCDIR: The directory to upload the documentation to +set -e +echo "Publishing documentation from branch $CI_BUILD_REF to $DOCDIR" + +# We need a custom wrapper around SSH to use our settings, and ssh-agent for the key +eval $(ssh-agent -s) +echo "${COQDOC_KEY}" | tr -d '\r' | ssh-add - +export GIT_SSH=$(readlink -e "$(dirname "$0")/ssh") + +# Enable tracing mode *after* we did the secret key stuff above +set -x diff --git a/build/ssh b/build/ssh new file mode 100755 index 00000000..735146c0 --- /dev/null +++ b/build/ssh @@ -0,0 +1,3 @@ +#!/bin/bash +_DIR=$(readlink -e "$(dirname "$0")") +exec ssh -o StrictHostKeyChecking=yes -o UserKnownHostsFile="${_DIR}/ssh_host_keys" "$@" -- GitLab