From c6438cf1a22d7ab73301000a05ca0de342f9f164 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 5 Jul 2024 09:36:11 +0200 Subject: [PATCH] Add CI testing using Github Actions (#514) The "build" job tests all supported architectures under Linux, using cross-compilation and QEMU to run the small test suite. It also tests AArch64 under macOS, natively. The "oldest" and "latest" jobs test compatibility with specific versions of Coq. They just build the proof and the extracted OCaml code, but they do not run any test. --- .github/workflows/build.yml | 64 ++++++++++ .github/workflows/latest.yml | 36 ++++++ .github/workflows/oldest.yml | 34 ++++++ tools/runner.sh | 225 +++++++++++++++++++++++++++++++++++ 4 files changed, 359 insertions(+) create mode 100644 .github/workflows/build.yml create mode 100644 .github/workflows/latest.yml create mode 100644 .github/workflows/oldest.yml create mode 100755 tools/runner.sh diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml new file mode 100644 index 0000000000..6a429cfa39 --- /dev/null +++ b/.github/workflows/build.yml @@ -0,0 +1,64 @@ +name: Build + +on: + push: + branches: + - 'master' + pull_request: + workflow_dispatch: + +jobs: + linux: + runs-on: ubuntu-latest + strategy: + matrix: + target: [aarch64, arm, ppc, riscv, x86_32, x86_64] + env: + target: ${{ matrix.target }} + os: linux + jobs: 4 + opamroot: /home/coq/.opam + container: + image: coqorg/coq:8.17.1 + options: --user root + steps: + - name: Checkout + uses: actions/checkout@v4 + with: + submodules: true + - name: OS dependencies + run: tools/runner.sh system_install + - name: OPAM dependencies + run: tools/runner.sh opam_install menhir + - name: Configure + run: tools/runner.sh configure + - name: Build + run: tools/runner.sh build + - name: Test default configuration + run: tools/runner.sh test1 + - name: Test alternate configuration + run: tools/runner.sh test2 + - name: Test alternate configuration 2 + run: tools/runner.sh test3 + macos: + runs-on: macos-latest + env: + target: aarch64 + os: macos + jobs: 3 + configopts: -ignore-coq-version -ignore-ocaml-version + steps: + - name: Checkout + uses: actions/checkout@v4 + with: + submodules: true + - name: OS dependencies + run: brew install coq menhir ocaml + - name: Configure + run: tools/runner.sh configure + - name: Build + run: tools/runner.sh build + - name: Test default configuration + run: tools/runner.sh test1 + - name: Test alternate configuration + run: tools/runner.sh test2 diff --git a/.github/workflows/latest.yml b/.github/workflows/latest.yml new file mode 100644 index 0000000000..507ed0c413 --- /dev/null +++ b/.github/workflows/latest.yml @@ -0,0 +1,36 @@ +name: Latest + +on: + push: + branches: + - 'master' + workflow_dispatch: + +jobs: + latest: + runs-on: ubuntu-latest + strategy: + matrix: + target: [aarch64, arm, ppc, riscv, x86_32, x86_64] + env: + target: ${{ matrix.target }} + os: linux + jobs: 4 + opamroot: /home/coq/.opam + configopts: -ignore-coq-version + container: + image: coqorg/coq:latest-ocaml-4.14-flambda + options: --user root + steps: + - name: Checkout + uses: actions/checkout@v4 + with: + submodules: true + - name: OPAM dependencies + run: tools/runner.sh opam_install menhir + - name: Configure + run: tools/runner.sh configure + - name: Build + run: tools/runner.sh build_ccomp + - name: Check proof + run: tools/runner.sh check_proof diff --git a/.github/workflows/oldest.yml b/.github/workflows/oldest.yml new file mode 100644 index 0000000000..95b59e0a16 --- /dev/null +++ b/.github/workflows/oldest.yml @@ -0,0 +1,34 @@ +name: Oldest + +on: + push: + branches: + - 'master' + workflow_dispatch: + +jobs: + latest: + runs-on: ubuntu-latest + strategy: + matrix: + target: [aarch64, arm, ppc, riscv, x86_32, x86_64] + env: + target: ${{ matrix.target }} + os: linux + jobs: 4 + opamroot: /home/coq/.opam + configopts: -ignore-coq-version + container: + image: coqorg/coq:8.12 + options: --user root + steps: + - name: Checkout + uses: actions/checkout@v4 + with: + submodules: true + - name: OPAM dependencies + run: tools/runner.sh opam_install menhir + - name: Configure + run: tools/runner.sh configure + - name: Build + run: tools/runner.sh build_ccomp diff --git a/tools/runner.sh b/tools/runner.sh new file mode 100755 index 0000000000..aa72e13460 --- /dev/null +++ b/tools/runner.sh @@ -0,0 +1,225 @@ +# Tell the tools to use only ASCII in diagnostic outputs +export LC_ALL=C + +# Stop on error +set -e + +# Simulators + +simu_aarch64="qemu-aarch64 -L /usr/aarch64-linux-gnu" +simu_armsf="qemu-arm -L /usr/arm-linux-gnueabi" +simu_armhf="qemu-arm -L /usr/arm-linux-gnueabihf" +simu_ppc32="qemu-ppc -L /usr/powerpc-linux-gnu -cpu G4" +simu_rv64="qemu-riscv64 -L /usr/riscv64-linux-gnu" +# simu_x86_32="qemu-i386 -L /usr/i686-linux-gnu" + +# Fatal error + +Fatal() { + echo "FATAL ERROR: $@" 1>&2 + exit 2 +} + +# Validate input parameters + +if test -z "$target"; then Fatal 'Missing $target value'; fi +if test -z "$os"; then Fatal 'Missing $os value'; fi +if test -z "$jobs"; then jobs=1; fi + +# Set up OPAM (if requested) + +if test -n "$opamroot"; then + export OPAMROOT="$opamroot" + eval `opam env --safe` +fi + +# Install additional system packages + +System_install() { + case "$target,$os" in + aarch64,linux) + sudo apt-get update + sudo apt-get -y install qemu-user gcc-aarch64-linux-gnu + ;; + arm,linux) + sudo apt-get update + sudo apt-get -y install qemu-user gcc-arm-linux-gnueabi gcc-arm-linux-gnueabihf + ;; + ppc,linux) + sudo apt-get update + sudo apt-get -y install qemu-user gcc-powerpc-linux-gnu + ;; + riscv,linux) + sudo apt-get update + sudo apt-get -y install qemu-user gcc-riscv64-linux-gnu + ;; + x86_32,linux) + sudo apt-get update + sudo apt-get -y install gcc-multilib + ;; + x86_64,linux) + ;; + aarch64,macos) + ;; + x86_64,macos) + ;; + x86_32,windows) + ;; + x86_64,windows) + ;; + esac +} + +# Install additional OPAM packages + +OPAM_install() { + if test -n "$*"; then + opam install -y $* + fi +} + +# Run configure script + +Configure() { + echo "Configuration parameters:" + echo " Target architecture \"$target\" (variable \$target)" + echo " Host OS \"$os\" (variable \$os)" + echo " Configure options \"$configopts\" (variable \$configopts)" + echo "" + case "$target,$os" in + aarch64,linux) + ./configure $configopts -toolprefix aarch64-linux-gnu- aarch64-linux + ;; + arm,linux) + ./configure $configopts -toolprefix arm-linux-gnueabihf- arm-eabihf + ;; + ppc,linux) + ./configure $configopts -toolprefix powerpc-linux-gnu- ppc-linux + ;; + riscv,linux) + ./configure $configopts -toolprefix riscv64-linux-gnu- rv64-linux + ;; + x86_32,linux) + ./configure $configopts x86_32-linux + ;; + x86_64,linux) + ./configure $configopts -clightgen x86_64-linux + ;; + aarch64,macos) + ./configure $configopts -clightgen aarch64-macos + ;; + x86_64,macos) + ./configure $configopts x86_64-macos + ;; + x86_32,windows) + ./configure $configopts x86_32-cygwin + ;; + x86_64,windows) + ./configure $configopts x86_64-cygwin + ;; + *) + Fatal "Unknown configuration \"$target\" - \"$os\"" + ;; + esac +} + +# Full build (including standard library) + +Build_all() { + make -j$jobs all +} + +# Coq + OCaml build (no standard library) + +Build_ccomp() { + make depend + make -j$jobs proof + make -j$jobs ccomp +} + +# Recheck proof using coqchk + +Check_proof() { + output=`mktemp` + trap "rm -f $output" 0 INT + if make check-proof > $output 2>&1 + then echo "Check proof: success" + else echo "Check proof: FAILURE"; cat $output; exit 2 + fi +} + +# Rebuild compcert.ini and the standard library with a different configuration +# Don't rebuild ccomp + +Rebuild_runtime() { + ./configure $* + make compcert.ini + make -C runtime -s clean + make -C runtime -j$jobs all +} + +# Run the test suite. +# First parameter: name of simulator to use (if any) +# Second parameter: compilation options (if any) + +Run_test() { + make -C test -s clean + make -C test CCOMPOPTS="$2" -j$jobs all + make -C test SIMU="$1" test +} + +# Rounds of testing. +# First parameter: round number (1, 2, ...) + +Run_test_round() { +case "$target,$os" in + aarch64,linux) + case "$1" in + 1) Run_test "$simu_aarch64" "";; + 2) Run_test "$simu_aarch64" "-Os";; + esac;; + aarch64,macos) + case "$1" in + 1) Run_test "" "";; + 2) Run_test "" "-Os";; + esac;; + arm,linux) + case "$1" in + 1) Run_test "$simu_armhf" "-marm";; + 2) Run_test "$simu_armhf" "-mthumb";; + 3) Rebuild_runtime -toolprefix arm-linux-gnueabi- arm-eabi + Run_test "$simu_armsf" "-marm";; + esac;; + ppc,linux) + case "$1" in + 1) Run_test "$simu_ppc32" "";; + 2) Run_test "$simu_ppc32" "-Os";; + esac;; + riscv,linux) + case "$1" in + 1) Run_test "$simu_rv64" "";; + 2) Run_test "$simu_rv64" "-Os";; + esac;; + x86_32,*|x86_64,*) + case "$1" in + 1) Run_test "" "";; + 2) Run_test "" "-Os";; + esac;; + *) + Fatal "Unknown configuration \"$target\" - \"$os\"" +esac +} + +case "$1" in + system_install) System_install;; + opam_install) shift; OPAM_install "$@";; + configure) Configure;; + build) Build_all;; + test1) Run_test_round 1;; + test2) Run_test_round 2;; + test3) Run_test_round 3;; + build_ccomp) Build_ccomp;; + check_proof) Check_proof;; + *) Fatal "Unknown CI instruction: $1"; exit 1;; +esac +