Add packaging for standalone files

.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:

.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:

.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

.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

.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:

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,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
@@ -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"

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"