diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 5e131187..d596f18c 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,10 @@ 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'] + exclude: # work around https://github.com/coq-community/docker-coq/issues/59 + - coq-version: '8.5' + test-location: 'standalone' runs-on: ubuntu-latest concurrency: @@ -117,6 +130,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}" "$@" }