From 4217c4bb4fc35d70cac091c43ce5d6c1cf89dbed Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Thu, 19 Oct 2023 16:48:07 -0700
Subject: [PATCH] Also test standalone builds on CI

---
 .github/workflows/ci.yml  | 28 +++++++++++++++++++++++-----
 Makefile                  |  9 ++++++++-
 examples/Makefile         |  3 ---
 examples/init-settings.sh |  3 +++
 4 files changed, 34 insertions(+), 9 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 0f51ce51..51e1051e 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -19,7 +19,7 @@ jobs:
       fail-fast: false
       matrix:
         python-version: [3.5, 3.6, 3.7, 3.8, 3.11]
-        test-location: ['installed', 'local']
+        test-location: ['installed', 'local', 'standalone']
         env:
         - { COQ_VERSION: "8.15.0", COQ_PACKAGE: "coq-8.14.0", PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-08", os: "ubuntu-20.04" }
         - { COQ_VERSION: "8.14.1", COQ_PACKAGE: "coq-8.14.1", PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-08", os: "ubuntu-20.04" }
@@ -58,22 +58,32 @@ jobs:
     - name: make doctests
       run: make doctests PYTHON3=python
       if: ${{ matrix.python-version != '2.7' }}
-    - name: install package building deps
+    - name: install package building deps (pip)
       run: |
         python -m pip install setuptools wheel twine
       if: ${{ matrix.test-location == 'installed' }}
-    - name: Build package
+    - name: install package building deps (standalone)
+      run: |
+        python -m pip install pyinstaller
+      if: ${{ matrix.test-location == 'standalone' }}
+    - name: Build package (dist)
       run: make dist
       if: ${{ matrix.test-location == 'installed' }}
+    - name: Build package (standalone)
+      run: make standalone
+      if: ${{ matrix.test-location == 'standalone' }}
     - name: Test install
       run: python -m pip install .
       if: ${{ matrix.test-location == 'installed' }}
     - name: Test (local)
       run: make print-support && make has-all-tests && make check PYTHON=python CAT_ALL_LOGS=1
-      if: ${{ matrix.test-location != 'installed' }}
+      if: ${{ matrix.test-location == 'local' }}
     - name: Test (installed)
       run: make print-support && make has-all-tests && make check PYTHON=python FIND_BUG=coq-bug-minimizer CAT_ALL_LOGS=1
       if: ${{ matrix.test-location == 'installed' }}
+    - name: Test (standalone)
+      run: make print-support && make has-all-tests && make check PYTHON=python FIND_BUG=dist/coq-bug-minimizer/coq-bug-minimizer CAT_ALL_LOGS=1
+      if: ${{ matrix.test-location == 'standalone' }}
 
   docker-build:
     strategy:
@@ -81,7 +91,7 @@ jobs:
       matrix:
         coq-version: ['dev', '8.18', '8.17', '8.16', '8.15', '8.14', '8.13', '8.12', '8.11', '8.10', '8.9', '8.8', '8.7', '8.6', '8.5', '8.4']
         ocaml-version: ['default']
-        test-location: ['installed', 'local']
+        test-location: ['installed', 'local', 'standalone']
 
     runs-on: ubuntu-latest
     concurrency:
@@ -117,6 +127,14 @@ jobs:
             python3 -m pip install .
             endGroup
             make check PYTHON=python3 FIND_BUG=coq-bug-minimizer CAT_ALL_LOGS=1
+          elif [ "${{ matrix.test-location }}" == "standalone" ]; then
+            startGroup 'install package building deps'
+            python3 -m pip install pyinstaller
+            endGroup
+            startGroup 'Build package'
+            make standalone PYTHON=python3
+            endGroup
+            make check PYTHON=python3 FIND_BUG=dist/coq-bug-minimizer/coq-bug-minimizer CAT_ALL_LOGS=1
           else
             make check PYTHON=python3 CAT_ALL_LOGS=1
           fi
diff --git a/Makefile b/Makefile
index d45e45f9..54f97f3a 100644
--- a/Makefile
+++ b/Makefile
@@ -1,5 +1,12 @@
+FIND_BUG?=
+ifneq (,$(strip $(FIND_BUG)))
+FULL_FIND_BUG:=$(abspath $(shell which '$(FIND_BUG)'))
+else
+FULL_FIND_BUG=$(FIND_BUG)
+endif
+
 has-all-tests check print-support::
-	$(MAKE) -C examples $@
+	$(MAKE) -C examples $@ FIND_BUG='$(FULL_FIND_BUG)'
 
 .PHONY: has-all-tests check print-support
 
diff --git a/examples/Makefile b/examples/Makefile
index 4a273dfe..9f2f3315 100644
--- a/examples/Makefile
+++ b/examples/Makefile
@@ -101,9 +101,6 @@ COQLIB_V_FILES:=$(wildcard $(COQC_COQLIB)/theories/Init/*.v)
 COQLIB_GLOB_FILES:=$(wildcard $(COQC_COQLIB)/theories/Init/*.glob)
 COQLIB_PRELUDE_V_FILE:=$(wildcard $(COQC_COQLIB)/theories/Init/Prelude.v)
 COQLIB_PRELUDE_GLOB_FILE:=$(wildcard $(COQC_COQLIB)/theories/Init/Prelude.glob)
-FIND_BUG?=
-
-export FIND_BUG
 
 .PHONY: check
 check::
diff --git a/examples/init-settings.sh b/examples/init-settings.sh
index 1e9b00c8..a3e5ca5d 100755
--- a/examples/init-settings.sh
+++ b/examples/init-settings.sh
@@ -14,6 +14,7 @@ if [ -z "${FIND_BUG}" ]; then
         ${PYTHON} "${FIND_BUG_PY}" "$@"
     }
 else
+    export FIND_BUG="$(cd "$DIR" && realpath "$(which "${FIND_BUG}")")"
     function find_bug() {
         "${FIND_BUG}" "$@"
     }
@@ -26,6 +27,7 @@ if [ -z "${MINIMIZE_REQUIRES}" ]; then
         ${PYTHON} "${MINIMIZE_REQUIRES_PY}" "$@"
     }
 else
+    export MINIMIZE_REQUIRES="$(cd "$DIR" && realpath "$(which "${MINIMIZE_REQUIRES}")")"
     function minimize_requires() {
         "${MINIMIZE_REQUIRES}" "$@"
     }
@@ -38,6 +40,7 @@ if [ -z "${ABSOLUTIZE_IMPORTS}" ]; then
         ${PYTHON} "${ABSOLUTIZE_IMPORTS_PY}" "$@"
     }
 else
+    export ABSOLUTIZE_IMPORTS="$(cd "$DIR" && realpath "$(which "${ABSOLUTIZE_IMPORTS}")")"
     function absolutize_imports() {
         "${ABSOLUTIZE_IMPORTS}" "$@"
     }