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 +