From 767e9cffdaa9760eb73f8ff4ed94afb2b55510c9 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 15 Nov 2021 14:41:06 +0100
Subject: [PATCH] chore: CI: check test binary as well

---
 .github/workflows/ci.yml | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index ce54f071a6..2aec0ed3e5 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -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