From 4066b517d99f71645305d668e15131e11a5600f0 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Fri, 25 Apr 2025 01:01:11 +0800
Subject: [PATCH 1/2] adapts CI to correct propagate exit code

---
 .github/workflows/docker-build-and-test.yml | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/docker-build-and-test.yml b/.github/workflows/docker-build-and-test.yml
index 83efbfa4..69e8945b 100644
--- a/.github/workflows/docker-build-and-test.yml
+++ b/.github/workflows/docker-build-and-test.yml
@@ -26,17 +26,23 @@ jobs:
     - name: List Docker images
       run: docker images
 
-    - name: Run container and execute lake build
+    - name: Start container (in background)
+      run: docker run --name test-container -dti veil/latest
+
+    - name: Execute lake build
       id: run-container
       run: |
-        docker run --name test-container -dti veil/latest
+        set +e # stop this script from aborting if a command fails, s.t., the exit code can be captured
         docker exec test-container bash -c 'cd veil && /root/.elan/bin/lake build || exit $?'
         echo "exitcode=$?" >> $GITHUB_OUTPUT
+
+    - name: Stop container and cleanup docker
+      if: ${{ always() }}
+      run: |
         docker stop test-container
         docker rm test-container
 
-    - name: Report status
+    - name: Report exit code
       if: ${{ steps.run-container.outcome == 'failure' }}
       run: |
-        echo "The lake build process exited with a non-zero status."
-
+        echo "The lake build process exited with the non-zero exit code ${{ steps.run-container.outputs.exitcode }}."

From ff7342eef533ed5b1190ec88035e14544de4539d Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Fri, 25 Apr 2025 01:02:48 +0800
Subject: [PATCH 2/2] trivial commit to trigger CI

---
 .github/workflows/docker-build-and-test.yml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/.github/workflows/docker-build-and-test.yml b/.github/workflows/docker-build-and-test.yml
index 69e8945b..c48deb24 100644
--- a/.github/workflows/docker-build-and-test.yml
+++ b/.github/workflows/docker-build-and-test.yml
@@ -44,5 +44,4 @@ jobs:
 
     - name: Report exit code
       if: ${{ steps.run-container.outcome == 'failure' }}
-      run: |
-        echo "The lake build process exited with the non-zero exit code ${{ steps.run-container.outputs.exitcode }}."
+      run: echo "The lake build process exited with the non-zero exit code ${{ steps.run-container.outputs.exitcode }}."