diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 1bafef34be82937b64e8d2be289d80b2907d30ff..948fdb8faca97c27d49efd7936290abd1d3dc0a2 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -21,23 +21,23 @@ iris: only: - master -vio: - stage: quickbuild - tags: - - coq - script: > - cd coq/ra/; - coqc -v; - time make -j8 TIMED=y quick 2>&1 | tee build-log-vio.txt; - cat build-log-vio.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-vio.txt - only: - - master - cache: - paths: - - coq/ra/*.vio - artifacts: - paths: - - coq/ra/build-time-vio.txt +# vio: +# stage: quickbuild +# tags: +# - coq +# script: > +# cd coq/ra/; +# coqc -v; +# time make -j8 TIMED=y quick 2>&1 | tee build-log-vio.txt; +# cat build-log-vio.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time-vio.txt +# only: +# - master +# cache: +# paths: +# - coq/ra/*.vio +# artifacts: +# paths: +# - coq/ra/build-time-vio.txt # vio2vo: # stage: quickcheck