From b15955f2a286660cbfe17661622dc389713642d6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 9 Nov 2023 11:53:48 -0800 Subject: [PATCH] Add packaging for standalone files In preparation for automatically deploying them to release pages. --- .github/workflows/coq-alpine.yml | 8 ++++++++ .github/workflows/coq-debian.yml | 8 ++++++++ .github/workflows/coq-macos.yml | 10 ++++++++++ .github/workflows/coq-windows.yml | 11 ++++++++++- .github/workflows/docker-coq.yml | 7 +++++++ Makefile.standalone | 20 ++++++++++++++++++++ etc/ci/mktemp_d.sh | 28 ++++++++++++++++++++++++++++ 7 files changed, 91 insertions(+), 1 deletion(-) create mode 100755 etc/ci/mktemp_d.sh diff --git a/.github/workflows/coq-alpine.yml b/.github/workflows/coq-alpine.yml index 35d4842f93..6ab7f719ae 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: make 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 b67b17a77a..774f3725bd 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 9eb32fe5fc..fc7317b7d7 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 @@ -69,6 +69,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' @@ -90,6 +94,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..31191de7cc 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,11 @@ CAMLOPT_PERF ?= $(OCAMLOPTP) CAMLOPT_PERF_SHOW:=OCAMLOPTP endif +PACKAGE ?= standalone.tar.gz +PACKAGE_CMD ?= tar -czvf +PACKAGE_CMD_FUNC ?= $(PACKAGE_CMD) $(1) $(2) +MKTEMP_D ?= etc/ci/mktemp_d.sh + ENSURE_STACK_LIMIT := . etc/ensure_stack_limit.sh || true .PHONY: \ @@ -26,6 +33,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 +101,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="$$(TMPDIR="$$(pwd)" $(MKTEMP_D))"; \ + $(MAKE) -f $(SELF) install-standalone-$* BINDIR="$$standalonedir" && \ + cd "$$standalonedir" && \ + $(call PACKAGE_CMD_FUNC,../$(PACKAGE),./*) && \ + cd ../ && \ + rm -rf "$$standalonedir" diff --git a/etc/ci/mktemp_d.sh b/etc/ci/mktemp_d.sh new file mode 100755 index 0000000000..b549cdd5da --- /dev/null +++ b/etc/ci/mktemp_d.sh @@ -0,0 +1,28 @@ +#!/bin/sh + +# Written mostly by GPT-4 https://web.archive.org/web/20231111233735/https://chat.openai.com/share/8098af96-4a10-4083-bf47-7f9e8cc333ed + +# Check if $RANDOM is available +if [ -z "$RANDOM" ]; then + random="$$" +else + random="$RANDOM" +fi + +# Try to use mktemp if available +if command -v mktemp > /dev/null; then + # MacOS and some BSDs require a template for mktemp + if [ "$(uname)" = "Darwin" ] || [ "$(uname)" = "FreeBSD" ]; then + temp_dir="$(mktemp -d "${TMPDIR:-/tmp}/tmp.XXXXXX")" + else + temp_dir="$(mktemp -d 2>/dev/null || mktemp -d -t 'tmp')" + fi +else + # Fallback: Create a directory with a random name in TMPDIR or /tmp + dir="${TMPDIR:-/tmp}/tmp.$random" + mkdir -p "$dir" + temp_dir="$dir" +fi + +# Output the path of the created directory +printf "%s\n" "$temp_dir"