aboutsummaryrefslogtreecommitdiffstats
path: root/.gitlab-ci.yml
diff options
context:
space:
mode:
Diffstat (limited to '.gitlab-ci.yml')
-rw-r--r--.gitlab-ci.yml23
1 files changed, 23 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index b3bb418f..6da3a91d 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -306,3 +306,26 @@ pages: # TODO: change to "deploy" when "build" succeeds (or integrate with "buil
rules:
- if: '$CI_COMMIT_BRANCH == "master"'
when: always
+
+build_aarch64_coq13:
+ stage: build
+ image: coqorg/coq:8.13.2-ocaml-4.11.1-flambda
+ before_script:
+ - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
+ - sudo apt-get -y install gcc-aarch64-linux-gnu qemu-user
+ - eval `opam config env`
+ - opam update
+ - opam install -y menhir
+ script:
+ - ./config_aarch64.sh
+ - make -j "$NJOBS"
+ rules:
+ - if: '$CI_COMMIT_BRANCH == "kvx-work"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "kvx-work-ssa"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "kvx-work-velus"'
+ when: always
+ - if: '$CI_COMMIT_BRANCH == "master"'
+ when: always
+ - when: manual