Upload rolling pre-releases

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>

.github/workflows/ci.yml

@@ -33,7 +33,7 @@ jobs:
               run: |
                 sudo apt-get update
                 sudo apt-get install --yes time
-            - uses: ocaml/setup-ocaml@v2
+            - uses: ocaml/setup-ocaml@v3
               with:
                 ocaml-compiler: ${{ matrix.ocaml-compiler }}
             - uses: actions/cache@v4
@@ -53,7 +53,7 @@ jobs:
                 # Workaround for https://github.com/tlaplus/tlapm/issues/88
                 set +e
                 for ((attempt = 1; attempt <= 5; attempt++)); do
-                  rm -rf _build
+                  make clean
                   make
                   if [ $? -eq 0 ]; then
                     make release
@@ -81,10 +81,10 @@ jobs:
             - name: Check proofs in TLA+ examples
               run: |
                 mkdir -p "$DEPS_DIR"
-                cp ./_build/tlaps*.tar.gz "$DEPS_DIR/tlaps.tar.gz"
-                tar -xzf "$DEPS_DIR/tlaps.tar.gz" -C "$DEPS_DIR"
-                rm "$DEPS_DIR/tlaps.tar.gz"
-                mv $DEPS_DIR/tlaps* "$DEPS_DIR/tlapm-install"
+                cp ./_build/tlapm*.tar.gz "$DEPS_DIR/tlapm.tar.gz"
+                tar -xzf "$DEPS_DIR/tlapm.tar.gz" -C "$DEPS_DIR"
+                rm "$DEPS_DIR/tlapm.tar.gz"
+                mv $DEPS_DIR/tlapm* "$DEPS_DIR/tlapm-install"
                 SKIP=(
                   # General proof failure
                   "specifications/Bakery-Boulangerie/Bakery.tla"

.github/workflows/rolling-prerelease.yml

@@ -0,0 +1,70 @@
+name: Rolling Pre-release
+on:
+  push:
+    branches: [main]
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+env:
+  DUNE_BUILD_DIR: "_build"
+  OCAML_VERSION: "5.1.0"
+jobs:
+  publish:
+    environment: release
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        os: [ubuntu-latest, macos-latest]
+    steps:
+    - name: Clone repo
+      uses: actions/checkout@v4
+    - name: Install deps on Ubuntu
+      if: matrix.os == 'ubuntu-latest'
+      run: sudo apt-get install --yes time
+    - uses: ocaml/setup-ocaml@v3
+      with:
+        ocaml-compiler: ${{ env.OCAML_VERSION }}
+    - uses: actions/cache@v4
+      id: cache
+      with:
+        path: _build_cache
+        key: ${{ runner.os }}_build_cache
+    - name: Build TLAPM
+      run: |
+        eval $(opam env)
+        make opam-deps
+        make opam-deps-opt
+        # Workaround for https://github.com/tlaplus/tlapm/issues/88
+        set +e
+        for ((attempt = 1; attempt <= 5; attempt++)); do
+          make clean
+          make
+          if [ $? -eq 0 ]; then
+            make release RELEASE_VERSION=${{ vars.ROLLING_PRERELEASE_VERSION }}
+            exit $?
+          fi
+        done
+        exit 1
+    - name: "Upload release"
+      run: |
+        kernel=$(uname -s)
+        if [ "$kernel" == "Linux" ]; then
+          OS_TYPE=linux-gnu
+        elif [ "$kernel" == "Darwin" ]; then
+          OS_TYPE=darwin
+        else
+          echo "Unknown OS: $kernel"
+          exit 1
+        fi
+        HOST_CPU=$(uname -m)
+        TLAPM_ZIP=tlapm-${{ vars.ROLLING_PRERELEASE_VERSION }}-$HOST_CPU-$OS_TYPE.tar.gz
+        echo $TLAPM_ZIP
+        ls -lh ${{ env.DUNE_BUILD_DIR }}
+        cat ${{ env.DUNE_BUILD_DIR }}/tlapm-release-version
+        ## Adapted from https://github.com/tlaplus/tlaplus repository
+        ## Crawl release id
+        DRAFT_RELEASE=$(curl -sS -H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" https://api.github.com/repos/${{ github.repository }}/releases --header "Content-Type: application/json" | jq '.[]| select(.name=="${{ vars.ROLLING_PRERELEASE_GITHUB_NAME }}") | .id')
+        ## Delete old assets and upload replacement assets (if delete fails we still try to upload the new asset)
+        ID=$(curl -sS -H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" https://api.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE/assets --header "Content-Type: application/json"  | jq '.[]| select(.name == "$TLAPM_ZIP") | .id')
+        curl -sS -X DELETE -H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" https://api.github.com/repos/${{ github.repository }}/releases/assets/$ID
+        curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://uploads.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE/assets?name=$TLAPM_ZIP --upload-file ${{ env.DUNE_BUILD_DIR }}/$TLAPM_ZIP

DEVELOPING.md

@@ -7,10 +7,8 @@ It uses the [Dune](https://dune.build/) build system for OCaml, with [Make](http
 
 Release Channels
 ----------------
-You can find official versioned releases on the [GitHub Releases page](https://github.com/tlaplus/tlapm/releases).
-
-Official releases lag the current development frontier by quite some time; thus, you might prefer to clone & build TLAPM yourself, as described below.
-Plans exist to make rolling pre-releases available in the near future.
+Past versioned releases can be downloaded from the [GitHub Releases page](https://github.com/tlaplus/tlapm/releases).
+For the latest development version, download the builds attached to the [1.6.0 rolling pre-release](https://github.com/tlapm/tlapm/releases/tag/1.6.0-pre) or follow the instructions below to build TLAPM from source.
 
 Dependencies
 ------------

Makefile

@@ -10,11 +10,11 @@ ifeq ($(OS_TYPE),Cygwin)
 	HOST_OS=cygwin
 endif
 HOST_CPU=$(shell uname -m)
-RELEASE_NAME=tlaps-$$RELEASE_VERSION-$(HOST_CPU)-$(HOST_OS)
-RELEASE_FILE=$(RELEASE_NAME).tar.gz
 
 PREFIX=$(OPAM_SWITCH_PREFIX)
 
+DUNE_BUILD_DIR=_build
+
 all: build
 
 opam-update: # Update the package lists and install updates.
@@ -55,29 +55,43 @@ install:
 	dune install --prefix=$(PREFIX)
 	make -C $(PREFIX)/lib/tlapm/ -f Makefile.post-install
 
-release:
-	rm -rf _build/tlaps-release-dir _build/tlaps-release-version
-	dune install --relocatable --prefix _build/tlaps-release-dir
-	make -C _build/tlaps-release-dir/lib/tlapm -f Makefile.post-install
+TLAPM_RELEASE_DIR_NAME=tlapm
+TLAPM_RELEASE_DIR=$(DUNE_BUILD_DIR)/$(TLAPM_RELEASE_DIR_NAME)
+$(TLAPM_RELEASE_DIR): build
+#	rm -rf $(TLAPM_RELEASE_DIR)
+	dune install --relocatable --prefix $(TLAPM_RELEASE_DIR)
+	make -C $(TLAPM_RELEASE_DIR)/lib/tlapm -f Makefile.post-install
 	cd test && env \
-		USE_TLAPM=../_build/tlaps-release-dir/bin/tlapm \
-		USE_LIB=../_build/tlaps-release-dir/lib/tlapm/stdlib \
+		USE_TLAPM=../$(TLAPM_RELEASE_DIR)/bin/tlapm \
+		USE_LIB=../$(TLAPM_RELEASE_DIR)/lib/tlapm/stdlib \
 		./TOOLS/do_tests fast/basic
-	RELEASE_VERSION="$$(_build/tlaps-release-dir/bin/tlapm --version)" \
-		&& rm -rf _build/$(RELEASE_FILE) \
-		&& mv _build/tlaps-release-dir _build/$(RELEASE_NAME) \
-		&& (cd _build/ && tar -czf $(RELEASE_FILE) $(RELEASE_NAME)) \
-		&& rm -rf _build/$(RELEASE_NAME) \
-		&& echo $$RELEASE_VERSION > _build/tlaps-release-version
 
-release-print-version:
-	@cat _build/tlaps-release-version
+$(TLAPM_RELEASE_DIR).tar.gz: $(TLAPM_RELEASE_DIR)
+	cd $(DUNE_BUILD_DIR) && tar -czf $(TLAPM_RELEASE_DIR_NAME).tar.gz $(TLAPM_RELEASE_DIR_NAME)
+
+# Use RELEASE_VERSION from Make CLI args; if not present, use TLAPM build version
+# Override variable like "make release RELEASE_VERSION=1.6.0"
+TLAPM_VERSION_FILE = $(DUNE_BUILD_DIR)/tlapm-release-version
+$(TLAPM_VERSION_FILE): $(TLAPM_RELEASE_DIR)
+	if [ -z "$(RELEASE_VERSION)" ]; then \
+		RELEASE_VERSION=$$($(TLAPM_RELEASE_DIR)/bin/tlapm --version); \
+	fi; \
+	echo $${RELEASE_VERSION} > $(TLAPM_VERSION_FILE)
+
+release: $(TLAPM_RELEASE_DIR).tar.gz $(TLAPM_VERSION_FILE)
+	TLAPM_RELEASE_VERSION="$$(cat $(TLAPM_VERSION_FILE))"; \
+	TLAPM_RELEASE_NAME=tlapm-$${TLAPM_RELEASE_VERSION}-$(HOST_CPU)-$(HOST_OS); \
+	mv $(TLAPM_RELEASE_DIR).tar.gz $(DUNE_BUILD_DIR)/$${TLAPM_RELEASE_NAME}.tar.gz;
+
+release-print-version: $(TLAPM_VERSION_FILE)
+	RELEASE_VERSION="$$(cat $(TLAPM_VERSION_FILE))"; \
+	echo $${RELEASE_VERSION}
 
-release-print-file:
-	@RELEASE_VERSION="$$(cat _build/tlaps-release-version)" && echo $(RELEASE_FILE)
+release-print-file: $(TLAPM_VERSION_FILE)
+	cat $(TLAPM_VERSION_FILE)
 
 clean:
 	dune clean
 
-.PHONY: all build check test test-inline test-fast test-fast-basic install release release-print-version release-print-file clean
+.PHONY: all build check test test-inline test-fast test-fast-basic install $(TLAPM_VERSION_FILE) release release-print-version release-print-file clean
 

README.md

@@ -10,8 +10,8 @@ For information on TLA⁺ generally, see http://tlapl.us.
 
 Installation & Use
 ------------------
-Versioned releases can be downloaded from the [GitHub Releases page](https://github.com/tlaplus/tlapm/releases).
-If you instead prefer to use the latest development version, follow the instructions in [`DEVELOPING.md`](DEVELOPING.md) to build & install TLAPM.
+Past versioned releases can be downloaded from the [GitHub Releases page](https://github.com/tlaplus/tlapm/releases).
+For the latest development version, download the builds attached to the [1.6.0 rolling pre-release](https://github.com/tlapm/tlapm/releases/tag/1.6.0-pre) or follow the instructions in [`DEVELOPING.md`](DEVELOPING.md) to build TLAPM from source.
 
 Once TLAPM is installed, run `tlapm --help` to see documentation of the various command-line parameters.
 Check the proofs in a simple example spec in this repo by running: