diff --git a/.github/workflows/coq-alpine.yml b/.github/workflows/coq-alpine.yml index 43effc9e03..b4ac54246f 100644 --- a/.github/workflows/coq-alpine.yml +++ b/.github/workflows/coq-alpine.yml @@ -63,6 +63,14 @@ jobs: name: generated-files-${{ matrix.alpine }} path: generated-files.tgz if: ${{ failure() }} + - name: package-standalone-ocaml + shell: alpine.sh {0} + run: etc/ci/github-actions-make.sh package-standalone-ocaml + - name: upload standalone files + uses: actions/upload-artifact@v3 + with: + name: standalone-${{ matrix.alpine }} + path: standalone.tar.gz - name: upload OCaml files uses: actions/upload-artifact@v3 with: diff --git a/.github/workflows/coq-debian.yml b/.github/workflows/coq-debian.yml index 7590d67ef9..474fe93e42 100644 --- a/.github/workflows/coq-debian.yml +++ b/.github/workflows/coq-debian.yml @@ -55,6 +55,14 @@ jobs: name: generated-files-${{ matrix.env.DEBIAN }} path: generated-files.tgz if: ${{ failure() }} + - name: package-standalone-ocaml + shell: in-debian-chroot.sh {0} + run: etc/ci/github-actions-make.sh package-standalone-ocaml + - name: upload standalone files + uses: actions/upload-artifact@v3 + with: + name: standalone-${{ matrix.env.DEBIAN }} + path: standalone.tar.gz - name: upload OCaml files uses: actions/upload-artifact@v3 with: diff --git a/.github/workflows/coq-macos.yml b/.github/workflows/coq-macos.yml index 31e03924cd..75a3085f94 100644 --- a/.github/workflows/coq-macos.yml +++ b/.github/workflows/coq-macos.yml @@ -61,6 +61,11 @@ jobs: eval $(opam env) etc/ci/github-actions-make.sh -j2 all + - name: package standalone files + run: | + eval $(opam env) + etc/ci/github-actions-make.sh package-standalone-ocaml + - name: only-test-amd64-files-lite run: | eval $(opam env) @@ -71,6 +76,11 @@ jobs: with: name: ExtractionOCaml path: src/ExtractionOCaml + - name: upload standalone files + uses: actions/upload-artifact@v3 + with: + name: standalone-macos + path: standalone.tar.gz - name: display timing info run: cat time-of-build-pretty.log - name: display per-line timing info diff --git a/.github/workflows/coq-windows.yml b/.github/workflows/coq-windows.yml index 83e482c62d..c92e137ecb 100644 --- a/.github/workflows/coq-windows.yml +++ b/.github/workflows/coq-windows.yml @@ -49,7 +49,7 @@ jobs: - name: Install System Dependencies run: | - %CYGWIN_ROOT%\setup-x86_64.exe -qnNdO -P time + %CYGWIN_ROOT%\setup-x86_64.exe -qnNdO -P time,zip shell: cmd - name: Work around https://github.com/actions/checkout/issues/766 @@ -68,6 +68,10 @@ jobs: run: | %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j${NJOBS} standalone-ocaml' shell: cmd + - name: package-standalone-ocaml + run: | + %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh package-standalone-ocaml PACKAGE=standalone.zip PACKAGE_CMD=zip' + shell: cmd - name: coq run: | %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j1 coq' @@ -89,6 +93,11 @@ jobs: with: name: ExtractionOCaml path: src/ExtractionOCaml + - name: upload standalone files + uses: actions/upload-artifact@v3 + with: + name: standalone-windows + path: standalone.zip - name: display timing info run: type time-of-build-pretty.log shell: cmd diff --git a/.github/workflows/docker-coq.yml b/.github/workflows/docker-coq.yml index 1818e0db0e..fd78b23d8e 100644 --- a/.github/workflows/docker-coq.yml +++ b/.github/workflows/docker-coq.yml @@ -66,6 +66,13 @@ jobs: name: generated-files-${{ matrix.env.COQ_VERSION }} path: generated-files.tgz if: ${{ failure() }} + - name: package-standalone-ocaml + run: etc/ci/github-actions-make.sh -f Makefile.standalone package-standalone-ocaml + - name: upload standalone files + uses: actions/upload-artifact@v3 + with: + name: standalone-docker-coq-${{ matrix.env.DOCKER_COQ_VERSION }} + path: standalone.tar.gz - name: upload OCaml files uses: actions/upload-artifact@v3 with: diff --git a/Makefile.standalone b/Makefile.standalone index b8871408e2..417e4dec3e 100644 --- a/Makefile.standalone +++ b/Makefile.standalone @@ -2,6 +2,8 @@ # files on .v files, so that we can compile them by invoking this # makefile directly even when Coq is not available +SELF := $(lastword $(MAKEFILE_LIST)) + include Makefile.config GHC?=ghc @@ -19,6 +21,10 @@ CAMLOPT_PERF ?= $(OCAMLOPTP) CAMLOPT_PERF_SHOW:=OCAMLOPTP endif +PACKAGE ?= standalone.tar.gz +PACKAGE_CMD ?= tar -czvf +PACKAGE_CMD_FUNC ?= $(PACKAGE_CMD) $(1) $(2) + ENSURE_STACK_LIMIT := . etc/ensure_stack_limit.sh || true .PHONY: \ @@ -26,6 +32,7 @@ ENSURE_STACK_LIMIT := . etc/ensure_stack_limit.sh || true standalone install-standalone uninstall-standalone \ standalone-ocaml install-standalone-ocaml uninstall-standalone-ocaml \ standalone-haskell install-standalone-haskell uninstall-standalone-haskell \ + package-standalone package-standalone-ocaml package-standalone-haskell \ # # pass -w -20 to disable the unused argument warning @@ -93,3 +100,15 @@ uninstall-standalone-ocaml uninstall-standalone-haskell: install-standalone: install-standalone-ocaml # install-standalone-haskell uninstall-standalone: uninstall-standalone-ocaml # uninstall-standalone-haskell + +package-standalone: package-standalone-ocaml # package-standalone-haskell + +package-standalone-ocaml package-standalone-haskell : package-standalone-% : + $(SHOW)'PACKAGE STANDALONE $*' + $(HIDE)rm -f "$(PACKAGE)" + +$(HIDE)standalonedir="$$(mktemp -d "$$(pwd)/standalone-tmp.XXXXX")"; \ + $(MAKE) -f $(SELF) install-standalone-$* BINDIR="$$standalonedir" && \ + cd "$$standalonedir" && \ + $(call PACKAGE_CMD_FUNC,../$(PACKAGE),./*) && \ + cd ../ && \ + rm -rf "$$standalonedir"