Merge pull request #167 from project-everest/_taramana_release_from_f…

…star_src Allow packaging and releasing from a F* source package
project-everest · Jan 24, 2025 · 66a869a · 66a869a
2 parents 3bd23af + 3642556
commit 66a869a
Show file tree

Hide file tree

Showing 5 changed files with 120 additions and 41 deletions.
diff --git a/.github/workflows/package-windows.yml b/.github/workflows/package-windows.yml
@@ -1,5 +1,6 @@
 name: Build everparse package (windows)
 on:
+  pull_request:
   workflow_dispatch:
     inputs:
       fstar_repo:
@@ -34,8 +35,8 @@ jobs:
       - uses: actions/checkout@master
         id: checkout
         with:
-          repository: ${{inputs.fstar_repo}}
-          ref: ${{inputs.fstar_ref}}
+          repository: ${{ inputs.fstar_repo || 'FStarLang/FStar' }}
+          ref: ${{ inputs.fstar_ref || 'master' }}
 
       - name: Check cache
         id: check-cache
@@ -132,8 +133,8 @@ jobs:
       - uses: actions/checkout@master
         with:
           path: karamel
-          repository: ${{inputs.karamel_repo}}
-          ref: ${{inputs.karamel_ref}}
+          repository: ${{ inputs.karamel_repo || 'FStarLang/karamel' }}
+          ref: ${{ inputs.karamel_ref || 'master' }}
 
       - uses: actions/download-artifact@v4
         with:

diff --git a/.gitignore b/.gitignore
@@ -16,6 +16,7 @@ bin/3d.exe
 
 # package.sh creates there
 __fstar-install
+fstar-src/fstar/*.checked
 everparse/**
 everparse_*.tar.gz
 everparse_*.zip
diff --git a/src/package/package.sh b/src/package/package.sh
@@ -121,34 +121,49 @@ make_everparse() {
     ## Setup F*. We need to locate a package, either it's already
     # there or we try to build one from the repo.
 
-    if ! [ -f fstar.tar.gz ] && ! [ -f fstar.zip ]; then
-      if ! [ -d FStar ]; then
-        git clone https://github.com/FStarLang/FStar --depth 1
-      fi
-      $MAKE -C FStar "$@" ADMIT=1
-      $MAKE -C FStar "$@" FSTAR_TAG= package
-      cp FStar/fstar.tar.gz . || cp FStar/fstar.zip .
-    fi
-
-    FSTAR_PKG_ROOT=__fstar-install
-    rm -rf "$FSTAR_PKG_ROOT"
-    mkdir -p "$FSTAR_PKG_ROOT"
-    if [ -f fstar.tar.gz ]; then
-      FSTAR_PKG=$(realpath fstar.tar.gz)
-      tar xzf $FSTAR_PKG -C "$FSTAR_PKG_ROOT"
-    elif [ -f fstar.zip ]; then
-      FSTAR_PKG=$(realpath fstar.zip)
-      pushd "$FSTAR_PKG_ROOT"
-      unzip -q "$FSTAR_PKG"
-      popd
-    else
-      echo "unexpected, no package?" >&2
-      exit 1
-    fi
-
+    FSTAR_PKG_ENVELOPE=__fstar-install
     # The package extracts into a fstar directory, and everything
     # is under there.
-    FSTAR_PKG_ROOT="$FSTAR_PKG_ROOT/fstar"
+    FSTAR_PKG_ROOT="$FSTAR_PKG_ENVELOPE/fstar"
+    FSTAR_SRC_PKG_ROOT=fstar-src/fstar
+    if ! [[ -d $FSTAR_PKG_ROOT ]] ; then
+        if [[ -d $FSTAR_SRC_PKG_ROOT ]] ; then
+            # build from a source package
+            dune_sandbox_opt=
+            if $is_windows ; then
+		# Dune crashes with "cannot delete sandbox." This fix comes
+		# from https://github.com/ocaml/dune/issues/8228#issuecomment-1642104172
+                dune_sandbox_opt=DUNE_CONFIG__BACKGROUND_SANDBOXES=disabled
+            fi
+            env $dune_sandbox_opt $MAKE -C $FSTAR_SRC_PKG_ROOT "$@" ADMIT=1
+            mkdir -p "$FSTAR_PKG_ROOT"
+            PREFIX="$(fixpath "$PWD/$FSTAR_PKG_ROOT")" $MAKE -C $FSTAR_SRC_PKG_ROOT install
+            $cp "$FSTAR_SRC_PKG_ROOT/LICENSE" "$FSTAR_PKG_ROOT/"
+        else
+            if ! [ -f fstar.tar.gz ] && ! [ -f fstar.zip ]; then
+                # build a binary package from a full F* clone
+                if ! [ -d FStar ]; then
+                    git clone https://github.com/FStarLang/FStar --depth 1
+                fi
+                $MAKE -C FStar "$@" ADMIT=1
+                $MAKE -C FStar "$@" FSTAR_TAG= package
+                $cp FStar/fstar.tar.gz . || $cp FStar/fstar.zip .
+            fi
+            mkdir -p "$FSTAR_PKG_ENVELOPE"
+            if [ -f fstar.tar.gz ]; then
+                FSTAR_PKG=$(realpath fstar.tar.gz)
+                tar xzf $FSTAR_PKG -C "$FSTAR_PKG_ENVELOPE"
+            elif [ -f fstar.zip ]; then
+                FSTAR_PKG=$(realpath fstar.zip)
+                pushd "$FSTAR_PKG_ENVELOPE"
+                unzip -q "$FSTAR_PKG"
+                popd
+            else
+                echo "unexpected, no package?" >&2
+                exit 1
+            fi
+        fi
+    fi
 
     export FSTAR_EXE=$(realpath $FSTAR_PKG_ROOT/bin/fstar.exe)
     export FSTAR_EXE=$(fixpath "$FSTAR_EXE")

diff --git a/src/package/release.sh b/src/package/release.sh
@@ -10,10 +10,12 @@ if [[ -z "$EVERPARSE_HOME" ]] ; then
     export EVERPARSE_HOME=$PWD
 fi
 
-# Necessary for gh to authenticate to GitHub
-if [[ -z "$GH_TOKEN" ]] ; then
-    echo Missing environment variable: GH_TOKEN
-    exit 1
+if [[ -z "$EVERPARSE_TEST_RELEASE" ]] ; then
+    # Necessary for gh to authenticate to GitHub
+    if [[ -z "$GH_TOKEN" ]] ; then
+        echo Missing environment variable: GH_TOKEN
+        exit 1
+    fi
 fi
 
 if [[ -z "$OS" ]] ; then
@@ -31,29 +33,89 @@ fi
 if [[ -z "$EVERPARSE_RELEASE_REPO" ]] ; then
     EVERPARSE_RELEASE_REPO=everparse
 fi
-remote="https://${GH_TOKEN}@github.com/${EVERPARSE_RELEASE_ORG}/${EVERPARSE_RELEASE_REPO}.git"
+if [[ -n ${GH_TOKEN} ]] ; then
+    remote="https://${GH_TOKEN}@github.com/${EVERPARSE_RELEASE_ORG}/${EVERPARSE_RELEASE_REPO}.git"
+else
+    remote="https://github.com/${EVERPARSE_RELEASE_ORG}/${EVERPARSE_RELEASE_REPO}.git"
+fi
 
 branchname=$(git rev-parse --abbrev-ref HEAD)
 git diff --staged --exit-code --ignore-cr-at-eol
 git diff --exit-code --ignore-cr-at-eol
 git fetch $remote --tags
 git pull $remote $branchname --ff-only
 
+git submodule init
+git submodule update
+git diff --staged --exit-code --ignore-cr-at-eol
+git diff --exit-code --ignore-cr-at-eol
+
+if [[ -d everest ]] ; then
+    # Install the Everest OPAM package dependencies
+    ./everest/everest --yes opam
+fi
+
+FSTAR_SRC_ENVELOPE=fstar-src
+FSTAR_SRC_PKG_ROOT=$FSTAR_SRC_ENVELOPE/fstar
+if $is_windows ; then
+    # On Windows, abort if the F* source package does not exist
+    if ! [[ -d "$FSTAR_SRC_PKG_ROOT" ]] ; then
+        echo 'Cannot find the F* source package. Please run this script on Linux first.'
+        exit 1
+    fi
+else
+    # On Linux, regenerate the F* source package
+    # FSTAR_TAG must be explicitly defined to an empty string
+    # to prevent the F* build system from mangling the name of
+    # the source archive
+    FSTAR_TAG= make -C FStar package-src ADMIT=1
+    rm -rf "$FSTAR_SRC_PKG_ROOT"
+    mkdir -p "$FSTAR_SRC_ENVELOPE"
+    tar -x -f FStar/fstar-src.tar.gz -C "$FSTAR_SRC_ENVELOPE/" -z
+    # Remove two empty directories that shouldn't be there, and whose names will clash on Windows
+    if [[ -d "$FSTAR_SRC_PKG_ROOT/none" ]] ; then rmdir "$FSTAR_SRC_PKG_ROOT/none" ; fi
+    if [[ -d "$FSTAR_SRC_PKG_ROOT/None" ]] ; then rmdir "$FSTAR_SRC_PKG_ROOT/None" ; fi
+    git add -- "$FSTAR_SRC_PKG_ROOT/"
+    if
+        ! {
+            git diff --staged --exit-code --ignore-cr-at-eol -- "$FSTAR_SRC_PKG_ROOT/" &&
+                git diff --exit-code --ignore-cr-at-eol -- "$FSTAR_SRC_PKG_ROOT/"
+        }
+    then
+        git commit -m "Refresh fstar-src"
+    fi
+fi
+
 everparse_version=$(sed 's!\r!!g' $EVERPARSE_HOME/version.txt)
 everparse_last_version=$(git show --no-patch --format=%h $everparse_version || true)
 everparse_commit=$(git show --no-patch --format=%h)
+needs_tag=false
 if [[ $everparse_commit != $everparse_last_version ]] ; then
+    if $is_windows ; then
+        echo "This commit does not match the latest release. release.sh must be run on Linux first."
+        exit 1
+    fi
     everparse_version=$($DATE '+v%Y.%m.%d')
     echo $everparse_version > $EVERPARSE_HOME/version.txt
     git add $EVERPARSE_HOME/version.txt
     git commit -m "Release $everparse_version"
+    needs_tag=true
     git tag $everparse_version
 fi
 export everparse_version
 #strip the v
 export everparse_nuget_version=${everparse_version:1}
 
-package_cmd="src/package/package.sh -zip -nuget"
+src/package/package.sh -zip -nuget
+
+if [[ -n "$EVERPARSE_TEST_RELEASE" ]] ; then
+    if $needs_tag ; then
+        echo "Release test mode, deleting the tag"
+        git tag -d $everparse_version
+    fi
+    echo "Release test succeeded!"
+    exit 0
+fi
 
 # push my commit and the tag
 git push $remote $branchname $everparse_version

diff --git a/src/package/release_linux.Dockerfile b/src/package/release_linux.Dockerfile
@@ -20,14 +20,14 @@ RUN { type -p curl >/dev/null || sudo apt-get install curl -y ; } \
 ADD --chown=opam:opam ./ $HOME/everparse/
 WORKDIR $HOME/everparse
 
-# Install opam package dependencies
-RUN eval $(opam env) && src/package/windows/everest.sh opam
-
 # Install other dependencies
-RUN sudo apt-get install --yes wget
+RUN sudo apt-get install --yes \
+  python-is-python3 \
+  wget
 
 # Build and publish the release
 ARG CI_THREADS=24
 ARG EVERPARSE_RELEASE_ORG=project-everest
 ARG EVERPARSE_RELEASE_REPO=everparse
-RUN --mount=type=secret,id=DZOMO_GITHUB_TOKEN eval $(opam env) && GH_TOKEN=$(sudo cat /run/secrets/DZOMO_GITHUB_TOKEN) EVERPARSE_RELEASE_ORG=$EVERPARSE_RELEASE_ORG EVERPARSE_RELEASE_REPO=$EVERPARSE_RELEASE_REPO make -j $CI_THREADS release
+ARG EVERPARSE_TEST_RELEASE=
+RUN --mount=type=secret,id=DZOMO_GITHUB_TOKEN eval $(opam env) && GH_TOKEN=$(sudo cat /run/secrets/DZOMO_GITHUB_TOKEN) EVERPARSE_RELEASE_ORG=$EVERPARSE_RELEASE_ORG EVERPARSE_RELEASE_REPO=$EVERPARSE_RELEASE_REPO EVERPARSE_TEST_RELEASE=$EVERPARSE_TEST_RELEASE make -j $CI_THREADS release