Skip to content

Commit

Permalink
Add packaging for standalone files (#1710)
Browse files Browse the repository at this point in the history
In preparation for automatically deploying them to release pages.
  • Loading branch information
JasonGross authored Nov 12, 2023
1 parent 47379ed commit f0c9395
Show file tree
Hide file tree
Showing 7 changed files with 91 additions and 1 deletion.
8 changes: 8 additions & 0 deletions .github/workflows/coq-alpine.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
8 changes: 8 additions & 0 deletions .github/workflows/coq-debian.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
10 changes: 10 additions & 0 deletions .github/workflows/coq-macos.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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
Expand Down
11 changes: 10 additions & 1 deletion .github/workflows/coq-windows.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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'
Expand All @@ -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
Expand Down
7 changes: 7 additions & 0 deletions .github/workflows/docker-coq.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
20 changes: 20 additions & 0 deletions Makefile.standalone
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -19,13 +21,19 @@ 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: \
perf-standalone \
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
Expand Down Expand Up @@ -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"
28 changes: 28 additions & 0 deletions etc/ci/mktemp_d.sh
Original file line number Diff line number Diff line change
@@ -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"

0 comments on commit f0c9395

Please sign in to comment.