Skip to content

Commit

Permalink
CI pkg:opam:native fix test
Browse files Browse the repository at this point in the history
https://docs.gitlab.com/ee/ci/yaml/#after_script

>Don’t affect the job’s exit code. If the script section succeeds and
the after_script times out or fails, the job exits with code 0 (Job
Succeeded).
  • Loading branch information
SkySkimmer committed Dec 10, 2024
1 parent 0e37250 commit 2fd29b2
Showing 1 changed file with 6 additions and 7 deletions.
13 changes: 6 additions & 7 deletions .gitlab-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -230,11 +230,15 @@ before_script:
extends: .auto-use-tags
# OPAM will build out-of-tree so no point in importing artifacts
script:
- if [ "$COQ_CI_NATIVE" = true ]; then opam install -y coq-native; fi
- opam pin add --kind=path coq-core.dev .
- opam pin add --kind=path rocq-core.dev .
- opam pin add --kind=path coq-stdlib.dev stdlib/
- opam pin add --kind=path coqide-server.dev .
- opam pin add --kind=path coqide.dev .
- if [ "$COQ_CI_NATIVE" = true ]; then echo "Definition f x := x + x." > test_native.v; fi
- if [ "$COQ_CI_NATIVE" = true ]; then coqc test_native.v; fi
- if [ "$COQ_CI_NATIVE" = true ]; then test -f .coq-native/Ntest_native.cmxs; fi
variables:
OPAM_VARIANT: "+flambda"
only: *full-ci
Expand Down Expand Up @@ -365,13 +369,8 @@ lint:

pkg:opam:native:
extends: .pkg:opam-template
before_script:
- opam install -y coq-native
after_script:
- eval $(opam env)
- echo "Definition f x := x + x." > test_native.v
- coqc -native-compiler yes test_native.v
- test -f .coq-native/Ntest_native.cmxs
variables:
COQ_CI_NATIVE: "true"

# broken, see eg https://gitlab.com/coq/coq/-/jobs/1754045983
# pkg:nix:deploy:
Expand Down

0 comments on commit 2fd29b2

Please sign in to comment.