chore: CI: check test binary as well

This commit is contained in:
Sebastian Ullrich 2021-11-15 14:41:06 +01:00
parent ad2fe8de80
commit 767e9cffda

View file

@ -29,6 +29,7 @@ jobs:
shell: nix-shell --arg pkgsDist "import (fetchTarball \"channel:nixos-19.03\") {{}}" --run "bash -euxo pipefail {0}"
llvm-url: https://github.com/leanprover/lean-llvm/releases/download/13.0.0/lean-llvm-x86_64-linux-gnu.tar.zst
prepare-llvm: script/prepare-llvm-linux.sh lean-llvm*
binary-check: ldd -v
- name: Linux
os: ubuntu-latest
check-stage3: true
@ -48,6 +49,7 @@ jobs:
CMAKE_OPTIONS: -DCMAKE_OSX_DEPLOYMENT_TARGET=10.14
llvm-url: https://github.com/leanprover/lean-llvm/releases/download/13.0.0/lean-llvm-x86_64-apple-darwin.tar.zst
prepare-llvm: script/prepare-llvm-macos.sh lean-llvm*
binary-check: otool -L
- name: Windows
os: windows-2022
release: true
@ -57,6 +59,7 @@ jobs:
CTEST_OPTIONS: --repeat until-pass:2
llvm-url: https://github.com/leanprover/lean-llvm/releases/download/13.0.0/lean-llvm-x86_64-w64-windows-gnu.tar.zst
prepare-llvm: script/prepare-llvm-mingw.sh lean-llvm*
binary-check: ldd
# complete all jobs
fail-fast: false
name: ${{ matrix.name }}
@ -124,14 +127,8 @@ jobs:
cmake .. ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
make -j4
make install
- name: Check binaries
if: matrix.os != 'macos-latest'
run: |
ldd -v lean-*/bin/* || true
- name: Check Binaries
if: matrix.name == 'macOS'
run: |
otool -L lean-*/bin/* || true
run: ${{ matrix.binary-check }} lean-*/bin/* || true
- name: List Install Tree
run: |
# omit contents of src/, Init/, ...
@ -155,6 +152,8 @@ jobs:
run: |
cd build/stage1
ctest -j4 --output-on-failure --timeout 300 ${{ matrix.CTEST_OPTIONS }} < /dev/null
- name: Check Test Binary
run: ${{ matrix.binary-check }} tests/compiler/534.lean.out
- name: Build Stage 2
run: |
cd build