From 6c35cef63f8243fd1831a269ba34add90df7b3fc Mon Sep 17 00:00:00 2001
From: iphydf <iphydf@users.noreply.github.com>
Date: Sat, 18 Nov 2023 05:46:19 +0000
Subject: [PATCH] chore: Add a compcert docker run script.

Useful for local runs. Does the same as CI, so if it fails on CI, this
can be used to test locally, avoiding slow CI round trips.
---
 .github/workflows/ci.yml         | 73 ++++++++++++--------------------
 other/docker/compcert/Dockerfile | 30 +++++++++++++
 other/docker/compcert/run        |  5 +++
 3 files changed, 62 insertions(+), 46 deletions(-)
 create mode 100644 other/docker/compcert/Dockerfile
 create mode 100755 other/docker/compcert/run

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 7db26ab256..eacf919ca5 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -60,16 +60,17 @@ jobs:
         with:
           file: other/docker/misra/Dockerfile
 
-  cimplefmt:
+  build-nacl:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v2
+      - name: Set up Docker Buildx
+        uses: docker/setup-buildx-action@v1
+      - name: Docker Build
+        uses: docker/build-push-action@v2
         with:
-          submodules: recursive
-      - name: Run cimplefmt
-        run: other/docker/cimplefmt/run -u $(find tox* -name "*.[ch]")
+          file: other/docker/autotools/Dockerfile
 
-  build-nacl:
+  build-tcc:
     runs-on: ubuntu-latest
     steps:
       - name: Set up Docker Buildx
@@ -77,7 +78,26 @@ jobs:
       - name: Docker Build
         uses: docker/build-push-action@v2
         with:
-          file: other/docker/autotools/Dockerfile
+          file: other/docker/tcc/Dockerfile
+
+  build-compcert:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Set up Docker Buildx
+        uses: docker/setup-buildx-action@v1
+      - name: Docker Build
+        uses: docker/build-push-action@v2
+        with:
+          file: other/docker/compcert/Dockerfile
+
+  cimplefmt:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v2
+        with:
+          submodules: recursive
+      - name: Run cimplefmt
+        run: other/docker/cimplefmt/run -u $(find tox* -name "*.[ch]")
 
   build-win32:
     runs-on: ubuntu-latest
@@ -125,45 +145,6 @@ jobs:
       - name: Build, test, and upload coverage
         run: .github/scripts/coverage-linux
 
-  build-tcc:
-    runs-on: ubuntu-latest
-    steps:
-      - name: Set up Docker Buildx
-        uses: docker/setup-buildx-action@v1
-      - name: Docker Build
-        uses: docker/build-push-action@v2
-        with:
-          file: other/docker/tcc/Dockerfile
-
-  build-compcert:
-    runs-on: ubuntu-latest
-    container: toxchat/compcert
-    steps:
-      - uses: actions/checkout@v2
-        with:
-          submodules: recursive
-      - name: Build with CompCert
-        run:
-          ccomp
-            -o send_message_test
-            -Wall -Werror
-            -Wno-c11-extensions
-            -Wno-unknown-pragmas
-            -Wno-unused-variable
-            -fstruct-passing -fno-unprototyped -g
-            auto_tests/auto_test_support.c
-            auto_tests/send_message_test.c
-            testing/misc_tools.c
-            toxav/*.c
-            toxcore/*.c
-            toxcore/*/*.c
-            toxencryptsave/*.c
-            third_party/cmp/*.c
-            -D__COMPCERT__ -DDISABLE_VLA -Dinline=
-            -lpthread $(pkg-config --cflags --libs libsodium opus vpx)
-      - name: Run the test
-        run: "./send_message_test | grep 'tox clients connected'"
-
   build-android:
     runs-on: ubuntu-latest
     steps:
diff --git a/other/docker/compcert/Dockerfile b/other/docker/compcert/Dockerfile
new file mode 100644
index 0000000000..bcc61387e1
--- /dev/null
+++ b/other/docker/compcert/Dockerfile
@@ -0,0 +1,30 @@
+FROM toxchat/compcert:latest
+
+WORKDIR /work
+COPY auto_tests/ /work/auto_tests/
+COPY testing/ /work/testing/
+COPY toxav/ /work/toxav/
+COPY toxcore/ /work/toxcore/
+COPY toxencryptsave/ /work/toxencryptsave/
+COPY third_party/ /work/third_party/
+
+SHELL ["/bin/bash", "-o", "pipefail", "-c"]
+
+RUN ccomp \
+ -o send_message_test \
+ -Wall -Werror \
+ -Wno-c11-extensions \
+ -Wno-unknown-pragmas \
+ -Wno-unused-variable \
+ -fstruct-passing -fno-unprototyped -g \
+ auto_tests/auto_test_support.c \
+ auto_tests/send_message_test.c \
+ testing/misc_tools.c \
+ toxav/*.c \
+ toxcore/*.c \
+ toxcore/*/*.c \
+ toxencryptsave/*.c \
+ third_party/cmp/*.c \
+ -D__COMPCERT__ -DDISABLE_VLA -Dinline= \
+ -lpthread $(pkg-config --cflags --libs libsodium opus vpx) \
+ && ./send_message_test | grep 'tox clients connected'
diff --git a/other/docker/compcert/run b/other/docker/compcert/run
new file mode 100755
index 0000000000..a061342816
--- /dev/null
+++ b/other/docker/compcert/run
@@ -0,0 +1,5 @@
+#!/bin/sh
+
+set -eux
+
+docker build -t toxchat/c-toxcore:compcert -f other/docker/compcert/Dockerfile .