aboutsummaryrefslogtreecommitdiffstats
path: root/.gitlab-ci.yml
diff options
context:
space:
mode:
Diffstat (limited to '.gitlab-ci.yml')
-rw-r--r--.gitlab-ci.yml350
1 files changed, 350 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
new file mode 100644
index 00000000..c8ccedb8
--- /dev/null
+++ b/.gitlab-ci.yml
@@ -0,0 +1,350 @@
+stages:
+ - build
+
+check-admitted:
+ stage: build
+ image: coqorg/coq:8.12.2-ocaml-4.11.2-flambda
+ before_script:
+ - eval `opam config env`
+ - opam update
+ - opam install -y menhir
+ script:
+ - ./config_x86_64.sh
+ - make check-admitted
+ 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
+
+build_x86_64:
+ stage: build
+ image: coqorg/coq:8.12.2-ocaml-4.11.2-flambda
+ before_script:
+ - eval `opam config env`
+ - opam update
+ - opam install -y menhir
+ script:
+ - ./config_x86_64.sh
+ - make -j "$NJOBS"
+ - make -j "$NJOBS" clightgen
+ - make -C test all test
+ - ulimit -s65536 && make -C test/monniaux/yarpgen
+ - ulimit -s65536 && make -C test/monniaux/csmith
+ 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
+
+build_ia32:
+ stage: build
+ image: coqorg/coq:8.12.2-ocaml-4.11.2-flambda
+ before_script:
+ - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
+ - sudo apt-get -y install gcc-multilib
+ - eval `opam config env`
+ - opam update
+ - opam install -y menhir
+ script:
+ - ./config_ia32.sh
+ - make -j "$NJOBS"
+ - make -j "$NJOBS" clightgen
+ - make -C test all test
+ - ulimit -s65536 && make -C test/monniaux/yarpgen BITS=32 TARGET_CC='gcc -m32'
+ - ulimit -s65536 && make -C test/monniaux/csmith TARGET_CC='gcc -m32'
+ 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
+
+build_aarch64:
+ stage: build
+ image: coqorg/coq:8.12.2-ocaml-4.11.2-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"
+ - make -j "$NJOBS" clightgen
+ - make -C test SIMU='qemu-aarch64 -L /usr/aarch64-linux-gnu' EXECUTE='qemu-aarch64 -L /usr/aarch64-linux-gnu' all test
+ - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='aarch64-linux-gnu-gcc' EXECUTE='qemu-aarch64 -L /usr/aarch64-linux-gnu'
+ - ulimit -s65536 && make -C test/monniaux/csmith TARGET_CC='aarch64-linux-gnu-gcc' EXECUTE='timeout 10s qemu-aarch64 -L /usr/aarch64-linux-gnu' CCOMPOPTS='-static' TARGET_CFLAGS='-static'
+ 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
+
+build_arm:
+ stage: build
+ image: coqorg/coq:8.12.2-ocaml-4.11.2-flambda
+ before_script:
+ - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
+ - sudo apt-get -y install gcc-arm-linux-gnueabi libc6-dev-armel-cross qemu-user
+ - eval `opam config env`
+ - opam update
+ - opam install -y menhir
+ script:
+ - ./config_arm.sh
+ - make -j "$NJOBS"
+ - make -j "$NJOBS" clightgen
+ - make -C test SIMU='qemu-arm -L /usr/arm-linux-gnueabi' EXECUTE='qemu-arm -L /usr/arm-linux-gnueabi' all test
+ - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='arm-linux-gnueabi-gcc' EXECUTE='qemu-arm -L /usr/arm-linux-gnueabi' BITS=32
+ - ulimit -s65536 && make -C test/monniaux/csmith TARGET_CC='arm-linux-gnueabi-gcc' EXECUTE='timeout 10s qemu-arm -L /usr/arm-linux-gnueabi' CCOMPOPTS='-static' TARGET_CFLAGS='-static' BITS=32
+ 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
+
+
+build_armhf:
+ stage: build
+ image: coqorg/coq:8.12.2-ocaml-4.11.2-flambda
+ before_script:
+ - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
+ - sudo apt-get -y install gcc-arm-linux-gnueabihf libc6-dev-armhf-cross qemu-user
+ - eval `opam config env`
+ - opam update
+ - opam install -y menhir
+ script:
+ - ./config_armhf.sh
+ - make -j "$NJOBS"
+ - make -j "$NJOBS" clightgen
+ - make -C test SIMU='qemu-arm -L /usr/arm-linux-gnueabihf' EXECUTE='qemu-arm -L /usr/arm-linux-gnueabihf' all test
+ - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='arm-linux-gnueabihf-gcc' EXECUTE='qemu-arm -L /usr/arm-linux-gnueabihf' BITS=32
+ - ulimit -s65536 && make -C test/monniaux/csmith TARGET_CC='arm-linux-gnueabihf-gcc' EXECUTE='timeout 10s qemu-arm -L /usr/arm-linux-gnueabihf' CCOMPOPTS='-static' TARGET_CFLAGS='-static' BITS=32
+ 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
+
+build_ppc:
+ stage: build
+ image: coqorg/coq:8.12.2-ocaml-4.11.2-flambda
+ before_script:
+ - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
+ - sudo apt-get -y install gcc-powerpc-linux-gnu wget ninja-build libglib2.0-dev libpixman-1-dev
+ - wget --no-verbose https://download.qemu.org/qemu-6.0.0.tar.xz
+ - tar xJf qemu-6.0.0.tar.xz
+ - (cd qemu-6.0.0 && ./configure --target-list=ppc-linux-user && make && sudo make install)
+ - eval `opam config env`
+ - opam update
+ - opam install -y menhir
+ script:
+ - ./config_ppc.sh
+ - make -j "$NJOBS"
+ - make -j "$NJOBS" clightgen
+ - qemu-ppc --version
+ - make -C test SIMU='qemu-ppc -L /usr/powerpc-linux-gnu -cpu 7400' EXECUTE='qemu-ppc -L /usr/powerpc-linux-gnu -cpu 7400' all test
+ - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='powerpc-linux-gnu-gcc' EXECUTE='qemu-ppc -L /usr/powerpc-linux-gnu -cpu 7400' BITS=32
+ - ulimit -s65536 && make -C test/monniaux/csmith TARGET_CC='powerpc-linux-gnu-gcc' EXECUTE='timeout 10s qemu-ppc -L /usr/powerpc-linux-gnu -cpu 7400'
+ 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
+
+build_ppc64:
+ stage: build
+ image: coqorg/coq:8.12.2-ocaml-4.11.2-flambda
+ before_script:
+ - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
+ - sudo apt-get -y install gcc-powerpc64-linux-gnu
+ - eval `opam config env`
+ - opam update
+ - opam install -y menhir
+ script:
+ - ./config_ppc64.sh
+ - make -j "$NJOBS"
+ - make -j "$NJOBS" clightgen
+ # - make -C test SIMU='qemu-ppc64 -L /usr/powerpc64-linux-gnu -cpu 7400' EXECUTE='qemu-ppc64 -L /usr/powerpc64-linux-gnu -cpu 7400' all test
+ # - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='powerpc64-linux-gnu-gcc' EXECUTE='qemu-ppc64 -L /usr/powerpc64-linux-gnu -cpu 7400' BITS=32
+ 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
+
+build_rv64:
+ stage: build
+ image: coqorg/coq:8.12.2-ocaml-4.11.2-flambda
+ before_script:
+ - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
+ - sudo apt-get -y install gcc-riscv64-linux-gnu qemu-user
+ - eval `opam config env`
+ - opam update
+ - opam install -y menhir
+ script:
+ - ./config_rv64.sh
+ - make -j "$NJOBS"
+ - make -j "$NJOBS" clightgen
+ - make -C test SIMU='qemu-riscv64 -L /usr/riscv64-linux-gnu' EXECUTE='qemu-riscv64 -L /usr/riscv64-linux-gnu' all test
+ - ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='riscv64-linux-gnu-gcc' EXECUTE='qemu-riscv64 -L /usr/riscv64-linux-gnu'
+ - ulimit -s65536 && make -C test/monniaux/csmith TARGET_CC='riscv64-linux-gnu-gcc' EXECUTE='timeout 10s qemu-riscv64 -L /usr/riscv64-linux-gnu' CCOMPOPTS='-static' TARGET_CFLAGS='-static'
+ 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
+
+build_rv32:
+ stage: build
+ image: coqorg/coq:8.12.2-ocaml-4.11.2-flambda
+ before_script:
+ - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
+ - sudo apt-get -y install gcc-riscv64-linux-gnu qemu-user
+ - eval `opam config env`
+ - opam update
+ - opam install -y menhir
+ script:
+ - ./config_rv32.sh -no-runtime-lib
+ - make -j "$NJOBS"
+ - make -j "$NJOBS" clightgen
+ 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
+
+build_kvx:
+ stage: build
+ image: coqorg/coq:8.12.2-ocaml-4.11.2-flambda
+ before_script:
+ - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
+ - sudo apt-get -y install sshpass openssh-client libzip4 lttng-tools liblttng-ctl-dev liblttng-ust-dev babeltrace libzip4
+ - ./.download_from_Kalray.sh
+ - (cd download ; rm -f *dkms*.deb *eclipse*.deb *llvm*.deb *board-mgmt* *oce-host* *pocl* *flash-util* *barebox* *-kann-* *-kaf-* *-stb-* *-opencv* *-eigen* *-task* *-blis* *-lz4*)
+ - sudo dpkg -i download/*.deb
+ - rm -rf download
+ - eval `opam config env`
+ - opam update
+ - opam install -y menhir
+ script:
+ - source /opt/kalray/accesscore/kalray.sh && ./config_kvx.sh
+ - source /opt/kalray/accesscore/kalray.sh && make -j "$NJOBS"
+ - make -j "$NJOBS" clightgen
+ - source /opt/kalray/accesscore/kalray.sh && make -C test CCOMPOPTS=-static SIMU='kvx-cluster -- ' EXECUTE='kvx-cluster -- ' all test
+ - source /opt/kalray/accesscore/kalray.sh && ulimit -s65536 && make -C test/monniaux/csmith TARGET_CC='kvx-cos-gcc' CCOMPOPTS="-Wl,--defsym=USER_STACK_SIZE=0x80000" EXECUTE="timeout 15s kvx-cluster -- "
+ - source /opt/kalray/accesscore/kalray.sh && ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='kvx-cos-gcc' EXECUTE='kvx-cluster -- ' CCOMPOPTS='-static' TARGET_CFLAGS='-static'
+ 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
+
+pages: # TODO: change to "deploy" when "build" succeeds (or integrate with "build_kvx" above ?)
+ stage: build
+ image: coqorg/coq:8.12.2-ocaml-4.11.2-flambda
+ before_script:
+ - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update
+ - sudo apt-get -y install sshpass openssh-client libzip4 lttng-tools liblttng-ctl-dev liblttng-ust-dev babeltrace
+ - ./.download_from_Kalray.sh
+ - (cd download ; rm -f *dkms*.deb *eclipse*.deb *llvm*.deb *board-mgmt* *oce-host* *pocl* *flash-util* *barebox* *-kann-* *-kaf-* *-stb-* *-opencv* *-eigen* *-task* *-blis* *-lz4*)
+ - sudo dpkg -i download/*.deb
+ - rm -rf download
+ - eval `opam config env`
+ - opam update
+ - opam install -y menhir
+ - opam repo add coq-released https://coq.inria.fr/opam/released
+ - opam install coq-coq2html
+ script:
+ - mkdir public
+ - source /opt/kalray/accesscore/kalray.sh && ./config_kvx.sh
+ - source /opt/kalray/accesscore/kalray.sh && make -j "$NJOBS"
+ - make -j "$NJOBS" clightgen
+ - source /opt/kalray/accesscore/kalray.sh && make documentation
+ - cp -rf doc/* public/
+ - mv doc/index-verimag.html public/index.html
+ artifacts:
+ paths:
+ - public
+ rules:
+ - if: '$CI_COMMIT_BRANCH == "master"'
+ when: always
+
+build_aarch64_coq13:
+ stage: build
+ image: coqorg/coq:8.13.2-ocaml-4.11.2-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"
+ - make -j "$NJOBS" clightgen
+ 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