Skip to content
Snippets Groups Projects
Commit 1cfa5d27 authored by Björn Brandenburg's avatar Björn Brandenburg
Browse files

CI: use alectryon for proof-state display

parent 6d39a63c
No related branches found
No related tags found
1 merge request!136Use alectryon to generate doc with proof state
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 8 deletions
.gitlab-ci.yml
+ 1
− 8
View file @ 1cfa5d27
...@@ -175,14 +175,7 @@ proof-state: ...@@ -175,14 +175,7 @@ proof-state:
dependencies: dependencies:
- build-for-process - build-for-process
script: script:
- find . -iname *.v ! -path './classic/*' | xargs -P ${NJOBS} -n 1 scripts/record-proof-state.py -c '-R . prosa -w -notation-overriden,-parsing' --timeout 20 - make alectryon
- scripts/intersperse-proof-state.py `find . -iname *.v ! -path './classic/*'`
- cd with-proof-state/
- ln -s ../scripts/
- ln -s ../_CoqProject
- ../create_makefile.sh
- make -j ${NJOBS}
- make html -j ${NJOBS} COQDOCEXTRAFLAGS=--plain-comments
- mv html ../with-proofs-and-proof-state - mv html ../with-proofs-and-proof-state
artifacts: artifacts:
name: "prosa-proof-state-$CI_COMMIT_REF_NAME" name: "prosa-proof-state-$CI_COMMIT_REF_NAME"
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment