Merge pull request #165 from mtzguido/master

actions: add package workflow

.github/workflows/package-linux.yml

@@ -0,0 +1,73 @@
+name: Build everparse package
+on:
+  workflow_dispatch:
+    inputs:
+      fstar_repo:
+        description: F* repository (use org/repo for Github repos)
+        default: 'FStarLang/FStar'
+        type: string
+        required: true
+      fstar_ref:
+        description: F* ref (branch, or tag, or commit hash)
+        default: 'master'
+        type: string
+        required: true
+      karamel_repo:
+        description: Karamel repository (use org/repo for Github repos)
+        default: 'FStarLang/karamel'
+        type: string
+        required: true
+      karamel_ref:
+        description: Karamel ref (branch, or tag, or commit hash)
+        default: 'master'
+        type: string
+        required: true
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  build:
+    runs-on: ubuntu-22.04
+    steps:
+      - uses: actions/checkout@master
+
+      - uses: actions/checkout@master
+        with:
+          path: FStar
+          repository: ${{inputs.fstar_repo}}
+          ref: ${{inputs.fstar_ref}}
+
+      - uses: actions/checkout@master
+        with:
+          path: karamel
+          repository: ${{inputs.karamel_repo}}
+          ref: ${{inputs.karamel_ref}}
+
+      - uses: ocaml/setup-ocaml@v3
+        with:
+          ocaml-compiler: 4.14.2
+
+      - name: Prepare
+        run: |
+          eval $(opam env)
+          sudo apt-get update || true
+          opam install --deps-only FStar/fstar.opam
+          sed -i '/"fstar"/d' karamel/karamel.opam
+          # ^ remove F* dependency of karamel, it is outdated and will conflict.
+          opam install --deps-only karamel/karamel.opam
+          opam install hex re sexplib
+          # ^ everparse deps
+
+      - name: Build package
+        run: |
+          eval $(opam env)
+          make package -kj$(nproc)
+
+      - uses: actions/upload-artifact@v4
+        with:
+          path: |
+            everparse*.zip
+            everparse*.tar.gz
+          name: everparse

.github/workflows/package-windows.yml

@@ -23,12 +23,143 @@ on:
         type: string
         required: true
 
-defaults:
-  run:
-    shell: bash
-
 jobs:
-  nop:
+  fstar-src:
+    ## NOTE: This is copied from build-src in the F* repo.
+
     runs-on: ubuntu-22.04
+    # We prefer slightly older Ubuntu so we get binaries that work on
+    # all more recent versions.
+    steps:
+      - uses: actions/checkout@master
+        id: checkout
+        with:
+          repository: ${{inputs.fstar_repo}}
+          ref: ${{inputs.fstar_ref}}
+
+      - name: Check cache
+        id: check-cache
+        uses: actions/cache/restore@v4
+        with:
+          path: fstar-src.tar.gz
+          key: FStar-src-${{steps.checkout.outputs.commit}}
+
+      - uses: ocaml/setup-ocaml@v3
+        if: steps.check-cache.outputs.cache-hit != 'true'
+        with:
+          ocaml-compiler: 4.14.2
+
+      - name: Prepare
+        if: steps.check-cache.outputs.cache-hit != 'true'
+        run: |
+          ./.scripts/get_fstar_z3.sh $HOME/bin
+          echo "PATH=$HOME/bin:$PATH" >> $GITHUB_ENV
+          opam install --deps-only ./fstar.opam
+
+      - name: Set F* version
+        if: steps.check-cache.outputs.cache-hit != 'true'
+        run: |
+          echo FSTAR_VERSION="$(git describe --tags --dirty)" >> $GITHUB_ENV
+
+      # NB: release workflow later adds version number to the name
+      - name: Build package
+        if: steps.check-cache.outputs.cache-hit != 'true'
+        run: |
+          eval $(opam env)
+          export FSTAR_TAG=
+          # ^ no tag in source package
+          make -skj$(nproc) package-src ADMIT=1
+
+      - name: Save
+        if: steps.check-cache.outputs.cache-hit != 'true'
+        uses: actions/cache/save@v4
+        with:
+          path: fstar-src.tar.gz
+          key: FStar-src-${{steps.checkout.outputs.commit}}
+
+      - uses: actions/upload-artifact@v4
+        with:
+          path: fstar-src.tar.gz
+          name: package-src
+
+  fstar-binary:
+    runs-on: [self-hosted, windows, X64, opam-2-3]
+    needs: fstar-src
     steps:
-      - run: exit 0
+      - name: clean
+        shell: C:\cygwin64\bin\bash.exe --login '{0}'
+        run: cd $GITHUB_WORKSPACE/ && rm -rf * && echo "There is a CR at the end of this line"
+
+      - uses: actions/download-artifact@v4
+        with:
+          name: package-src
+
+      # - name: Check cache
+      #   id: check-cache
+      #   uses: actions/cache/restore@v4
+      #   with:
+      #     path: fstar.zip
+      #     key: FStar-${{runner.os}}-${{ hashFiles('/fstar-src.tar.gz') }}
+
+      - run: cd $GITHUB_WORKSPACE && tar xzf fstar-src.tar.gz && echo ""
+        # if: steps.check-cache.outputs.cache-hit != 'true'
+        shell: C:\cygwin64\bin\bash.exe --login '{0}'
+
+      - name: Build a package
+        # if: steps.check-cache.outputs.cache-hit != 'true'
+        shell: C:\cygwin64\bin\bash.exe --login '{0}'
+        run: |
+          cd $GITHUB_WORKSPACE && cd fstar && eval $(opam env) && make clean && CC=x86_64-w64-mingw32-gcc.exe DUNE_CONFIG__BACKGROUND_SANDBOXES=disabled make -j$(nproc) package V=1 ADMIT=1 && mv fstar.zip .. && echo "There is a CR at the end of this line"
+        
+      # - name: Save
+      #   if: steps.check-cache.outputs.cache-hit != 'true'
+      #   uses: actions/cache/save@v4
+      #   with:
+      #     path: fstar.zip
+      #     key: FStar-${{runner.os}}-${{ hashFiles('/fstar-src.tar.gz') }}
+
+      - uses: actions/upload-artifact@v4
+        with:
+          name: fstar-package
+          path: fstar.zip
+
+  build:
+    runs-on: [self-hosted, windows, X64, opam-2-3]
+    needs: fstar-binary
+    steps:
+      - uses: actions/checkout@master
+
+      - uses: actions/checkout@master
+        with:
+          path: karamel
+          repository: ${{inputs.karamel_repo}}
+          ref: ${{inputs.karamel_ref}}
+
+      - uses: actions/download-artifact@v4
+        with:
+          name: fstar-package
+
+      - name: Prepare
+        # opam install --deps-only FStar/fstar.opam
+        # ^ relying on the fact that F* dependencies are already installed
+        if: false
+        # Disabling this, I get
+        # Error:  Package karamel has no version opam.
+        # but karamel.opam should refer to the file? This also did not
+        # work with karamel/karamel.opam (without cd'ing).
+        shell: C:\cygwin64\bin\bash.exe --login '{0}'
+        run: |
+          cd $GITHUB_WORKSPACE && eval $(opam env) && cd karamel && sed -i '/"fstar"/d' karamel.opam && opam install --deps-only karamel.opam && opam install hex re sexplib && echo ""
+
+      - name: Build package
+        shell: C:\cygwin64\bin\bash.exe --login '{0}'
+        run: |
+          cd $GITHUB_WORKSPACE && eval $(opam env) && CC=x86_64-w64-mingw32-gcc.exe make package -kj$(nproc) && echo ""
+
+      - uses: actions/upload-artifact@v4
+        with:
+          path: |
+            everparse*.zip
+            everparse*.tar.gz
+            everparse*.nupkg
+          name: everparse

src/package/package.sh

@@ -115,26 +115,36 @@ make_everparse() {
     export OTHERFLAGS='--admit_smt_queries true'
     #!!!!!
 
-    # Verify if F* and KaRaMeL are here
     cp0=$(which gcp >/dev/null 2>&1 && echo gcp || echo cp)
     cp="$cp0 --preserve=mode,timestamps"
 
-    ## Setup F*
+    ## 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 ]; then
+    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.tar.gz . || cp FStar/fstar.zip .
     fi
 
-    FSTAR_PKG=$(realpath fstar.tar.gz)
     FSTAR_PKG_ROOT=__fstar-install
     rm -rf "$FSTAR_PKG_ROOT"
     mkdir -p "$FSTAR_PKG_ROOT"
-    tar xzf $FSTAR_PKG -C "$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
 
     # The package extracts into a fstar directory, and everything
     # is under there.