Skip to content

Commit

Permalink
Add CI testing using Github Actions
Browse files Browse the repository at this point in the history
  • Loading branch information
@xavierleroy
xavierleroy committed Jul 5, 2024
1 parent 8f5fd33 commit 50770a3
Show file tree
Hide file tree
Showing 4 changed files with 359 additions and 0 deletions.
64 changes: 64 additions & 0 deletions .github/workflows/build.yml
View file
Original file line number Diff line number Diff line change
@@ -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
36 changes: 36 additions & 0 deletions .github/workflows/latest.yml
View file
Original file line number Diff line number Diff line change
@@ -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
34 changes: 34 additions & 0 deletions .github/workflows/oldest.yml
View file
Original file line number Diff line number Diff line change
@@ -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
225 changes: 225 additions & 0 deletions tools/runner.sh
View file
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit 50770a3

Please sign in to comment.