Merge pull request #311 from mtzguido/main

Restoring mac builds, packaging, devcontainer

.devcontainer/devcontainer.json

@@ -1,6 +1,6 @@
 {
   "name": "Pulse devcontainer (from cached base container)",
-  "image": "mtzguido/pulse-devcontainer:latest",
+  "image": "mtzguido/pulse-base-devcontainer:latest",
   "customizations": {
     "vscode": {
       "extensions": [
@@ -15,7 +15,6 @@
   },
   // Runs periodically and/or when content of repo changes
   "updateContentCommand": {
-    "build_plugin_and_lib": "make -j$(nproc)"
   },
   // These run only when the container is assigned to a user
   "postCreateCommand": {

.devcontainer/fromscratch/devcontainer.json

@@ -17,7 +17,6 @@
   },
   // Runs periodically and/or when content of repo changes
   "updateContentCommand": {
-    "build_plugin_and_lib": "make -j$(nproc)"
   },
   // These run only when the container is assigned to a user
   "postCreateCommand": {

.devcontainer/fromscratch/minimal.Dockerfile

@@ -1,4 +1,4 @@
-FROM ubuntu:23.10
+FROM ubuntu:24.04
 
 SHELL ["/bin/bash", "-c"]
 
@@ -45,25 +45,25 @@ RUN opam option depext-run-installs=true
 ENV OPAMYES=1
 RUN opam install --yes batteries zarith stdint yojson dune menhir menhirLib pprint sedlex ppxlib process ppx_deriving ppx_deriving_yojson memtrace
 
-# Get compiled Z3
-RUN wget -nv https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-ubuntu-16.04.zip \
- && unzip z3-4.8.5-x64-ubuntu-16.04.zip \
- && cp z3-4.8.5-x64-ubuntu-16.04/bin/z3 $HOME/bin/z3 \
- && rm -r z3-4.8.5-*
-
-# Get F* master and build
+# Get F* master and build (install opam deps too)
 RUN eval $(opam env) \
  && source $HOME/.profile \
  && git clone --depth=1 https://github.com/FStarLang/FStar \
  && cd FStar/ \
+ && opam install --deps-only ./fstar.opam \
  && make -j$(nproc) ADMIT=1 \
  && ln -s $(realpath bin/fstar.exe) $HOME/bin/fstar.exe
 
-# Get karamel master and build
+# Install z3 with F* script
+RUN ./FStar/.scripts/get_fstar_z3.sh $HOME/bin
+
+# Get karamel master and build (installing opam deps too, but ignoring fstar dependency)
 RUN eval $(opam env) \
  && source $HOME/.profile \
  && git clone --depth=1 https://github.com/FStarLang/karamel \
  && cd karamel/ \
+ && sed -i '/"fstar"/d' karamel.opam \
+ && opam install --deps-only ./karamel.opam \
  && .docker/build/install-other-deps.sh \
  && make -j$(nproc)
 

.github/workflows/nightly.yml

@@ -0,0 +1,108 @@
+name: Pulse nightly build
+on:
+  workflow_dispatch:
+  schedule:
+    - cron: '0 0 * * *'
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  linux:
+    runs-on: ubuntu-22.04
+    steps:
+      - uses: actions/checkout@master
+      - uses: actions/checkout@master
+        with:
+          path: FStar
+          repository: FStarLang/FStar
+
+      - uses: ocaml/setup-ocaml@v3
+        with:
+          ocaml-compiler: 4.14.2
+
+      - name: Prepare
+        run: |
+          ./FStar/.scripts/get_fstar_z3.sh $HOME/bin
+          echo "PATH=$HOME/bin:$PATH" >> $GITHUB_ENV
+          opam install --deps-only ./FStar/fstar.opam
+
+      - run: eval $(opam env) && .scripts/mk_package.sh
+      - uses: actions/upload-artifact@v4
+        with:
+          path: pulse-*.tar.gz
+          name: package-linux
+
+  mac:
+    runs-on: macos-14
+    steps:
+      - uses: actions/checkout@master
+      - uses: actions/checkout@master
+        with:
+          path: FStar
+          repository: FStarLang/FStar
+
+      - uses: ocaml/setup-ocaml@v3
+        with:
+          ocaml-compiler: 4.14.2
+
+      - name: Prepare
+        run: |
+          brew install opam bash gnu-getopt coreutils gnu-sed make
+          ./FStar/.scripts/get_fstar_z3.sh $HOME/bin
+          echo "PATH=$HOME/bin:$PATH" >> $GITHUB_ENV
+          opam install --deps-only ./FStar/fstar.opam
+
+      - run: eval $(opam env) && .scripts/mk_package.sh
+      - uses: actions/upload-artifact@v4
+        with:
+          path: pulse-*.tar.gz
+          name: package-mac
+
+  publish:
+    runs-on: ubuntu-latest
+    needs:
+      - linux
+      - mac
+    steps:
+      - uses: actions/checkout@master
+        with:
+          fetch-depth: 0 # full clone, so we can push objects
+
+      - name: Set up git
+        run: |
+          git config --global user.name "Dzomo, the Everest Yak"
+          git config --global user.email "[email protected]"
+
+      - uses: actions/download-artifact@v4
+        with:
+          path: artifacts
+          merge-multiple: true
+          # ^ Download all artifacts into the same dir.
+          # Each of them is a single file, so no clashes happen.
+
+      - name: Publish artifacts in nightly tag
+        run: |
+          git config --unset-all http.https://github.com/.extraheader
+          # ^ https://stackoverflow.com/questions/64374179/how-to-push-to-another-repository-in-github-actions
+
+          # We push nightly builds to a different repo (same org)
+          REPO="${{github.repository}}-nightly"
+          TAG=nightly-$(date -I)
+
+          # Create tag
+          git tag $TAG ${{github.sha}}
+
+          # Add new remote and push tag
+          git remote add nightly-repo https://${{secrets.DZOMO_GITHUB_TOKEN}}@github.com/$REPO
+          git push nightly-repo $TAG
+
+          # Create release
+          gh release create -R "$REPO" \
+            --generate-notes \
+            --target ${{ github.sha }} \
+            $TAG artifacts/*
+
+        env:
+          GH_TOKEN: ${{ secrets.DZOMO_GITHUB_TOKEN }}

.gitignore

@@ -21,3 +21,8 @@ BUILDLOG
 out
 _output
 _cache
+
+# For package building
+FStar
+_pak
+pulse.tar.gz

.scripts/mk_package.sh

@@ -0,0 +1,52 @@
+#!/bin/bash
+
+# This scripts builds a "standalone" package with F* and Pulse. It
+# does not include karamel as there is no way to install it and use it
+# without setting a KRML_HOME, which I would like to avoid. This will be
+# fixed soon.
+
+set -eux
+
+if [ "$(uname -s)" = "Darwin" ]; then
+MAKE="gmake -ksj$(nproc)"
+else
+MAKE="make -ksj$(nproc)"
+fi
+
+if ! [ -d FStar ]; then
+  git clone https://github.com/FStarLang/FStar --depth 1
+fi
+
+$MAKE -C FStar ADMIT=1
+export FSTAR_EXE=$(pwd)/FStar/bin/fstar.exe
+
+$MAKE ADMIT=1
+
+rm -rf _pak
+mkdir -p _pak/pulse
+$MAKE -C FStar install PREFIX=$(pwd)/_pak/pulse
+
+$MAKE install PREFIX=$(pwd)/_pak/pulse
+
+cat >_pak/pulse/bin/pulse << EOF
+#!/bin/bash
+
+# Pulse is really just F* + an include path. The pulse plugin
+# is loaded automatically by F* when needed (e.g. when processing
+# a #lang-pulse declaration).
+
+D=\$(dirname "\$0")
+
+exec \$D/fstar.exe --include "\$D/../lib/pulse" "\$@"
+EOF
+
+chmod +x _pak/pulse/bin/pulse
+
+KERNEL=$(uname -s)
+ARCH=$(uname -m)
+PAK=pulse-$KERNEL-$ARCH.tar.gz
+
+tar czf $PAK -C _pak .
+
+echo Done
+ls -l $PAK

Makefile

@@ -74,7 +74,7 @@ do-install: plugin lib-pulse
 	# Install plugin.
 	$(FSTAR_EXE) --ocamlenv \
 	  dune install --root=build/ocaml --prefix=$(abspath $(PREFIX))
-	# Install library (cp -u: don't copy unless newer, -p: preserve time/perms)
+	# Install library (cp -p: preserve time/perms)
 	# We install it flat. Note that lib/core is not included, but still some PulseCore
 	# checked files make it in. We could add:
 	#   \( -not -name 'PulseCore.*' \)
@@ -83,12 +83,13 @@ do-install: plugin lib-pulse
 	# to change their namespace.
 	find lib/pulse lib/common \
 		\( -name '*.fst' -o -name '*.fsti' -o -name '*.checked' -o -name '*.ml' \) -and \
-		-exec cp -p -u -t $(PREFIX)/lib/pulse/lib {} \;
+		-exec cp -p {} $(PREFIX)/lib/pulse/lib \;
 	# Set up fstar.include so users only include lib/pulse
 	echo 'lib' > $(PREFIX)/lib/pulse/fstar.include
 
 	# Install share/ too, as-is.
-	cp -p -t $(PREFIX) -r share/
+	mkdir -p share/pulse
+	cp -p -r share/pulse/* $(PREFIX)/share/pulse/
 
 .PHONY: clean
 clean: