From 8e06a296c5bae585dcdaa9de8b8b91f86d4b5915 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Thu, 31 Oct 2019 13:37:01 +0100
Subject: [PATCH] CI: build docs with interspersed proof state
---
.gitlab-ci.yml | 20 ++++++++++++++++++++
1 file changed, 20 insertions(+)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index df91fd024..f5811b6d4 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -84,3 +84,23 @@ proof-length:
image: python:3-alpine
script:
- scripts/proofloc.py --check --long-proofs scripts/known-long-proofs.json `find . -iname *.v`
+
+proof-state:
+ stage: process
+ image: mathcomp/mathcomp:1.9.0-coq-8.10
+ dependencies:
+ - 1.9.0-coq-8.10
+ script:
+ - find restructuring util -iname *.v | xargs -P ${NJOBS} -n 1 scripts/record-proof-state.py -c '-R . rt -w -notation-overriden,-parsing' --timeout 20
+ - scripts/intersperse-proof-state.py `find restructuring util -iname *.v`
+ - cd with-proof-state/
+ - ln -s ../scripts/
+ - ln -s ../_CoqProject
+ - ../create_makefile.sh
+ - make html -j ${NJOBS} COQDOCEXTRAFLAGS=--plain-comments
+ - mv html ../with-proofs-and-proof-state
+ artifacts:
+ name: "prosa-proof-state-$CI_COMMIT_REF_NAME"
+ paths:
+ - "with-proofs-and-proof-state/"
+ expire_in: 1 week
--
GitLab