Merge pull request #3637 from mtzguido/dev

Staged build, new CI, new packaging

.docker/dev-base.Dockerfile

@@ -0,0 +1,58 @@
+FROM ubuntu:24.04
+
+RUN apt-get update
+
+RUN apt-get install -y --no-install-recommends \
+      git \
+      sudo \
+      python3 \
+      python-is-python3 \
+      opam \
+      rustc \
+      curl \
+      ca-certificates \
+      rsync \
+      wget \
+      && apt-get clean -y
+
+# Install the relevant Z3 versions.
+COPY ./bin/get_fstar_z3.sh /usr/local/bin
+RUN get_fstar_z3.sh /usr/local/bin
+
+RUN useradd -ms /bin/bash user
+RUN echo 'user ALL=NOPASSWD: ALL' >> /etc/sudoers
+USER user
+WORKDIR /home/user
+
+# Install OCaml
+ARG OCAML_VERSION=4.14.2
+RUN opam init --compiler=$OCAML_VERSION --disable-sandboxing
+RUN opam env --set-switch | tee --append $HOME/.profile $HOME/.bashrc $HOME/.bash_profile
+RUN opam option depext-run-installs=true
+ENV OPAMYES=1
+
+# F* dependencies. This is the only place where we read a file from
+# the F* repo.
+ADD fstar.opam ./fstar.opam
+RUN opam install -j$(nproc) --confirm-level=unsafe-yes --deps-only ./fstar.opam && opam clean
+
+# Some karamel dependencies too. hex for everparse
+RUN opam install -j$(nproc) --confirm-level=unsafe-yes fix fileutils visitors camlp4 wasm ulex uucp ctypes ctypes-foreign hex && opam clean
+
+RUN sudo apt install time
+
+# Sigh, install dotnet. The setup-dotnet action does not
+# work on a container apparently.
+ENV DOTNET_ROOT /dotnet
+RUN wget -nv https://download.visualstudio.microsoft.com/download/pr/cd0d0a4d-2a6a-4d0d-b42e-dfd3b880e222/008a93f83aba6d1acf75ded3d2cfba24/dotnet-sdk-6.0.400-linux-x64.tar.gz && \
+    sudo mkdir -p $DOTNET_ROOT && \
+    sudo tar xf dotnet-sdk-6.0.400-linux-x64.tar.gz -C $DOTNET_ROOT && \
+    rm -f dotnet-sdk*.tar.gz
+RUN sudo ln -s $DOTNET_ROOT/dotnet /usr/local/bin/dotnet
+
+RUN rm fstar.opam # move up
+
+# install rust (move up and remove rustv)
+RUN curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
+RUN sudo apt-get update && sudo apt-get install --yes --no-install-recommends llvm-dev libclang-dev clang libgmp-dev pkg-config
+RUN . "$HOME/.cargo/env" && rustup component add rustfmt && cargo install bindgen-cli

.github/workflows/build-all.yml

@@ -0,0 +1,14 @@
+name: Build F* binaries (all archs)
+
+on:
+  workflow_call:
+  workflow_dispatch:
+
+jobs:
+  build-linux:
+    # This job also builds an (architecture-indepenendent) source package
+    # artifact.
+    uses: ./.github/workflows/build-linux.yml
+
+  build-macos:
+    uses: ./.github/workflows/build-macos.yml

.github/workflows/build-ci.yml

@@ -0,0 +1,72 @@
+name: Build F* (ci)
+
+# This builds F* for Linux for the purposes of CI. It runs on a
+# recent Ubuntu-based container and also generates a source package
+# and a repo snapshot. For the purposes of binary releases, see
+# build-linux.yml.
+
+on:
+  workflow_call:
+  workflow_dispatch:
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  build:
+    # Build an F* binary package: a fully-bootstrapped stage 2 compiler,
+    # with its plugins, a fully checked library (i.e. with .checked)
+    # files and compiled versions of fstar_lib and fstar_plugin_lib.
+    # We do not package a stage 1 compiler.
+    # runs-on: [self-hosted, linux, X64] # self-hosted so we use fast runners
+    runs-on: ubuntu-latest
+    container: mtzguido/dev-base
+    steps:
+      - name: Cleanup
+        run: sudo find . -delete
+      - run: echo "HOME=/home/user" >> $GITHUB_ENV
+      - uses: mtzguido/set-opam-env@master
+
+      - uses: actions/checkout@master
+        with:
+          path: FStar
+
+      - name: Produce all artifacts
+        run: |
+          # Note: we don't package Z3 for the CI artifact as the images
+          # already have the relevant Z3.
+          make -skj$(nproc) package package-src FSTAR_TAG= FSTAR_PACKAGE_Z3=false
+        working-directory: FStar
+
+      # Upload the archives.
+      - uses: actions/upload-artifact@v4
+        with:
+          path: FStar/fstar.tar.gz
+          name: fstar.tar.gz
+          retention-days: 3
+      - uses: actions/upload-artifact@v4
+        with:
+          path: FStar/fstar-src.tar.gz
+          name: fstar-src.tar.gz
+          retention-days: 3
+
+      # Upload full repo too, for stage3 check and Pulse. Note: we
+      # explicitly run 'make setlink-2' at this point to generate the out/
+      # directory, as the previous targets do not. Also, remove the
+      # previous archives so they don't blow up the size of this
+      # artifact.
+      - run: rm -f FStar/fstar*.tar.gz
+      - run: make setlink-2
+        working-directory: FStar
+
+      - uses: mtzguido/gci-upload@master
+        with:
+          name: fstar-repo
+          path: FStar
+          extra: --exclude=FStar/stage*/dune/_build
+          hometag: FSTAR
+
+      # FIXME: Ideally, we could upload the artifacts as soon as each of
+      # them is created, and start the subsequent jobs at that instant too.
+      # Is that even doable...?

.github/workflows/build-linux.yml

@@ -0,0 +1,58 @@
+name: Build F* (Linux)
+
+# This builds F* for Linux for a binary package release.
+# See build.yml for the build used in normal CI runs.
+
+on:
+  workflow_call:
+  workflow_dispatch:
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  build:
+    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
+
+      - uses: ocaml/setup-ocaml@v3
+        with:
+          ocaml-compiler: 4.14.2
+
+      - name: Prepare
+        run: |
+          ./.scripts/get_fstar_z3.sh $HOME/bin
+          echo "PATH=$HOME/bin:$PATH" >> $GITHUB_ENV
+          opam install --deps-only ./fstar.opam
+
+      - name: Set version
+        run: |
+          # Setting FSTAR_VERSION for nightly and release builds. If unset,
+          # we use $(version.txt)~dev. Setting it avoids the ~dev.
+          if [[ "${{github.workflow_ref}}" =~ "nightly.yml" ]]; then
+            echo FSTAR_VERSION="nightly-$(date -I)" >> $GITHUB_ENV
+          elif [[ "${{github.workflow_ref}}" =~ "release.yml" ]]; then
+            echo FSTAR_VERSION="$(cat version.txt)" >> $GITHUB_ENV
+          fi
+
+      # NB: release workflow later adds version number to the name
+      - name: Build packages
+        run: |
+          eval $(opam env)
+          KERNEL=$(uname -s)
+          ARCH=$(uname -m)
+          make -skj$(nproc) package     FSTAR_TAG=-$KERNEL-$ARCH
+          make -skj$(nproc) package-src FSTAR_TAG=
+
+      - uses: actions/upload-artifact@v4
+        with:
+          path: fstar-Linux-*
+          name: package-linux
+      - uses: actions/upload-artifact@v4
+        with:
+          path: fstar-src.tar.gz
+          name: package-src

.github/workflows/build-macos.yml

@@ -0,0 +1,46 @@
+name: Build F* (macos)
+
+on:
+  workflow_dispatch:
+  workflow_call:
+
+jobs:
+  build:
+    runs-on: macos-latest
+    steps:
+      - uses: actions/checkout@master
+
+      - uses: ocaml/setup-ocaml@v3
+        with:
+          ocaml-compiler: 4.14.2
+
+      - name: Prepare
+        run: |
+          brew install opam bash gnu-getopt coreutils gnu-sed make
+          ./.scripts/get_fstar_z3.sh $HOME/bin
+          echo "PATH=$HOME/bin:$PATH" >> $GITHUB_ENV
+          opam install --deps-only ./fstar.opam
+
+      - name: Set version
+        run: |
+          # Setting FSTAR_VERSION for nightly and release builds. If unset,
+          # we use $(version.txt)~dev. Setting it avoids the ~dev.
+          if [[ "${{github.workflow_ref}}" =~ "nightly.yml" ]]; then
+            echo FSTAR_VERSION="nightly-$(date -I)" >> $GITHUB_ENV
+          elif [[ "${{github.workflow_ref}}" =~ "release.yml" ]]; then
+            echo FSTAR_VERSION="$(cat version.txt)" >> $GITHUB_ENV
+          fi
+
+      # Note *g*make below!
+      # NB: release workflow later adds version number to the name
+      - name: Build package
+        run: |
+          eval $(opam env)
+          KERNEL=$(uname -s)
+          ARCH=$(uname -m)
+          gmake -skj$(nproc) package FSTAR_TAG=-$KERNEL-$ARCH
+
+      - uses: actions/upload-artifact@v4
+        with:
+          path: fstar-*
+          name: package-mac