From c1c282e2162d1e808dacbc06b3253522d4ce15b7 Mon Sep 17 00:00:00 2001 From: Andrew Helwer Date: Wed, 4 Dec 2024 14:36:14 -0500 Subject: [PATCH] Upload rolling pre-releases (#182) Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com> --- .github/workflows/ci.yml | 12 ++-- .github/workflows/rolling-prerelease.yml | 70 ++++++++++++++++++++++++ DEVELOPING.md | 6 +- Makefile | 52 +++++++++++------- README.md | 4 +- 5 files changed, 113 insertions(+), 31 deletions(-) create mode 100644 .github/workflows/rolling-prerelease.yml diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d33ca301..1074e64f 100644 --- a/.github/workflows/ci.yml +++ b/.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" diff --git a/.github/workflows/rolling-prerelease.yml b/.github/workflows/rolling-prerelease.yml new file mode 100644 index 00000000..4f111069 --- /dev/null +++ b/.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 diff --git a/DEVELOPING.md b/DEVELOPING.md index bbe78ff7..644f6b10 100644 --- a/DEVELOPING.md +++ b/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 ------------ diff --git a/Makefile b/Makefile index c23f1454..ca333260 100644 --- a/Makefile +++ b/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 diff --git a/README.md b/README.md index b8eb44f2..2b367a0c 100644 --- a/README.md +++ b/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: