Skip to content

Commit

Permalink
Fix artifacts for build:vio
Browse files Browse the repository at this point in the history
coq#17785 changed the artifact paths but
this job wasn't adapted.

Because of the workaround for
https://gitlab.com/gitlab-org/gitlab/issues/202505 this wasn't detected.
  • Loading branch information
SkySkimmer committed Dec 11, 2023
1 parent 9e3a56b commit d94d232
Showing 1 changed file with 1 addition and 7 deletions.
8 changes: 1 addition & 7 deletions .gitlab-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -168,7 +168,7 @@ before_script:
# put || exit 0 as a workaround if https://gitlab.com/gitlab-org/gitlab/issues/202505 reoccurs
# the validate:vio job is sometimes started before build:vio, without artifacts
# we ignore these spurious errors so if the job fails it's a real error
- cd _install_ci
- if test "$CI_JOB_NAME" = "validate:vio"; then tar xfj _build.tar.bz2 && cd _build/install/default; else cd _install_ci; fi
- find lib/coq/ -name '*.vo' -fprint0 vofiles
- xargs -0 --arg-file=vofiles bin/coqchk -o -m -coqlib lib/coq/ > ../coqchk.log 2>&1 || touch coqchk.failed
- tail -n 1000 ../coqchk.log # the log is too big for gitlab so pipe to a file and display the tail
Expand Down Expand Up @@ -333,7 +333,6 @@ build:base+async:
build:vio:
extends: .build-template:base:dev
variables:
COQ_EXTRA_CONF: "-native-compiler no"
COQ_DUNE_EXTRA_OPT: "-vio"
DUNE_TARGET: "vio world"
after_script:
Expand All @@ -342,11 +341,6 @@ build:vio:
only:
variables:
- ($FULL_CI == "true" && $UNRELIABLE =~ /enabled/)
artifacts:
when: always
paths:
- _install_ci
- dmesg.txt

lint:
stage: build
Expand Down

0 comments on commit d94d232

Please sign in to comment.