Merge branch 'master' into auto_github

Author: mtzguido

.github/workflows/build-linux.yml

@@ -12,7 +12,7 @@ defaults:
     shell: bash
 
 jobs:
-  build:
+  build-linux:
     runs-on: ubuntu-22.04
     # We prefer slightly older Ubuntu so we get binaries that work on
     # all more recent versions.
@@ -37,6 +37,7 @@ jobs:
             echo FSTAR_VERSION="nightly-$(date -I)" >> $GITHUB_ENV
           elif [[ "${{github.workflow_ref}}" =~ "release.yml" ]]; then
             echo FSTAR_VERSION="$(cat version.txt)" >> $GITHUB_ENV
+            echo FSTAR_RELEASE=1 >> $GITHUB_ENV
           fi
 
       # NB: release workflow later adds version number to the name
@@ -45,8 +46,10 @@ jobs:
           eval $(opam env)
           KERNEL=$(uname -s)
           ARCH=$(uname -m)
-          make -skj$(nproc) package     FSTAR_TAG=-$KERNEL-$ARCH
+          export FSTAR_TAG=-$KERNEL-$ARCH
+          make -skj$(nproc) package
           make -skj$(nproc) package-src FSTAR_TAG=
+          # ^ no tag in source package
 
       - uses: actions/upload-artifact@v4
         with:

.github/workflows/build-macos.yml

@@ -5,7 +5,7 @@ on:
   workflow_call:
 
 jobs:
-  build:
+  build-macos:
     runs-on: macos-latest
     steps:
       - uses: actions/checkout@master
@@ -29,6 +29,7 @@ jobs:
             echo FSTAR_VERSION="nightly-$(date -I)" >> $GITHUB_ENV
           elif [[ "${{github.workflow_ref}}" =~ "release.yml" ]]; then
             echo FSTAR_VERSION="$(cat version.txt)" >> $GITHUB_ENV
+            echo FSTAR_RELEASE=1 >> $GITHUB_ENV
           fi
 
       # Note *g*make below!
@@ -38,7 +39,8 @@ jobs:
           eval $(opam env)
           KERNEL=$(uname -s)
           ARCH=$(uname -m)
-          gmake -skj$(nproc) package FSTAR_TAG=-$KERNEL-$ARCH
+          export FSTAR_TAG=-$KERNEL-$ARCH
+          gmake -skj$(nproc) package
 
       - uses: actions/upload-artifact@v4
         with:

.gitignore

@@ -2,6 +2,7 @@
 /stage2/out
 /stage3
 /out
+/*.tar
 /*.tar.gz
 /*.zip
 /_pak*

.scripts/bin-install.sh

@@ -0,0 +1,52 @@
+#!/bin/bash
+
+# This is called by the Makefile *after* an installation into the
+# prefix, so we add the rest of the files that go into a binary package.
+
+set -eu
+
+windows () {
+  # This seems portable enough and does not trigger an
+  # undefined variable error (see set -u above) if $OS
+  # is unset (like in linux/mac). Note: OSX's bash is usually
+  # old and does not support '[ -v OS ]'.
+  [[ "${OS:-}" = "Windows_NT" ]]
+}
+
+if [ $# -ne 1 ]; then
+  echo "Usage: $0 <prefix>" >&2
+  exit 1
+fi
+
+PREFIX="$1"
+mkdir -p "$PREFIX"
+PREFIX="$(realpath "$PREFIX")"
+
+if ! [ -v FSTAR_PACKAGE_Z3 ] || ! [ "$FSTAR_PACKAGE_Z3" = false ]; then
+  .scripts/package_z3.sh "$PREFIX"
+fi
+
+if windows; then
+    # This dll is needed. It must be installed if we're packaging, as we
+    # must have run F* already, but it should probably be obtained from
+    # somewhere else..
+    LIBGMP=$(which libgmp-10.dll) || echo "error: libgmp-10.dll not found! Carrying on..." >&2
+    cp "$LIBGMP" "$PREFIX/bin"
+fi
+
+# License and extra files. Not there on normal installs, but present in
+# package.
+cp LICENSE* "$PREFIX"
+cp README.md "$PREFIX"
+cp INSTALL.md "$PREFIX"
+cp version.txt "$PREFIX"
+
+# Save the megabytes! Strip binaries
+STRIP=strip
+
+if windows; then
+  STRIP="$(pwd)/mk/winwrap.sh $STRIP"
+fi
+
+$STRIP "$PREFIX"/bin/* || true
+$STRIP "$PREFIX"/lib/fstar/z3-*/bin/* || true

.scripts/check-snapshot-diff.sh

@@ -60,11 +60,11 @@ download_z3() {
   z3_path="${base_name%.zip}/bin/z3"
   if [ "$kernel" = Windows ]; then z3_path="$z3_path.exe"; fi
 
-  pushd "$tmp_dir"
-  curl -L "$url" -o "$base_name"
+  pushd "$tmp_dir" > /dev/null
+  curl -s -L "$url" -o "$base_name"
 
   unzip -q "$base_name" "$z3_path"
-  popd
+  popd > /dev/null
   install -m0755 "$tmp_dir/$z3_path" "$destination_file_name"
   echo ">>> Installed Z3 $version to $destination_file_name"
 }
@@ -77,17 +77,17 @@ full_install_z3() {
   dest_dir="$3"
 
   mkdir -p "$dest_dir/z3-$version"
-  pushd "$dest_dir/z3-$version"
+  pushd "$dest_dir/z3-$version" > /dev/null
 
   echo ">>> Downloading Z3 $version from $url ..."
   base_name="$(basename "$url")"
-  curl -L "$url" -o "$base_name"
+  curl -s -L "$url" -o "$base_name"
 
   unzip -q "$base_name"
   mv "${base_name%.zip}"/* .
   rmdir "${base_name%.zip}"
   rm "$base_name"
-  popd
+  popd > /dev/null
 }
 
 usage() {

.scripts/get_fstar_z3.sh

@@ -1,11 +1,14 @@
 #!/usr/bin/env bash
 
+windows () {
+  [[ "${OS:-}" = "Windows_NT" ]]
+}
+
 if [[ -z "$FSTAR_VERSION" ]]; then
   FSTAR_VERSION=$(head -n 1 version.txt)~dev
 fi
 
-if [ "$OS" = "Windows_NT" ]
-then
+if windows; then
    if [ "$PROCESSOR_ARCHITECTURE" = "AMD64" ]
    then
      PLATFORM="Windows_x64"

.scripts/make_fstar_version.sh

@@ -1,29 +1,117 @@
 #!/bin/bash
 
+set -eu
+
+# This will just create a tar.gz or zip out of a directory.
+# You may want to look at src-install.sh and bin-install.sh
+# that generate the layouts for a source and binary package,
+# and are then packaged up with this script.
+
 if [ $# -ne 2 ]; then
-	echo "usage: $0 <install_root> <package_basename>" >&2
-	echo "Default format is tar.gz. Optionally set FSTAR_PACKAGE_FORMAT=zip to generate a zip instead." >&2
-	echo "Output filename is <package_basename> + proper extension." >&2
-	exit 1
+  exec >&2
+  echo "usage: $0 <install_root> <package_basename>"
+  echo "The archive format and command used depends on the system and installed tools,"
+  echo "see script for details."
+  echo "Optionally set FSTAR_PACKAGE_FORMAT to: "
+  echo " - 'zip': create a .zip via 'zip' command"
+  echo " - '7z': create a .zip via '7z' command"
+  echo " - 'tar.gz': create a .tar.gz, via calling"
+  echo "Output filename is <package_basename> + proper extension"
+  echo "If FSTAR_RELEASE is non-empty, we use maximum compression."
+  exit 1
 fi
 
 PREFIX="$1"
 ARCHIVE="$2"
 
+windows () {
+  # This seems portable enough and does not trigger an
+  # undefined variable error (see set -u above) if $OS
+  # is unset (like in linux/mac). Note: OSX's bash is usually
+  # old and does not support '[ -v OS ]'.
+  [[ "${OS:-}" = "Windows_NT" ]]
+}
+
+release () {
+  [[ -n "${FSTAR_RELEASE:-}" ]]
+}
+
+# Computes a (hopefully) sensible default for the current system
+detect_format () {
+  if windows; then
+    # Github actions runner do not have 'zip'
+    if which zip > /dev/null; then
+      FSTAR_PACKAGE_FORMAT=zip
+    elif which 7z > /dev/null; then
+      FSTAR_PACKAGE_FORMAT=7z
+    else
+      echo "error: no zip or 7z command found." >&2
+      exit 1
+    fi
+  else
+    FSTAR_PACKAGE_FORMAT=tar.gz
+  fi
+}
+
+# If unset, pick a default for the system.
+if ! [ -v FSTAR_PACKAGE_FORMAT ]; then
+  detect_format
+fi
+
+# Fix for stupid path confustion in windows
+if windows; then
+  WRAP=$(pwd)/mk/winwrap.sh
+else
+  WRAP=
+fi
+
 case $FSTAR_PACKAGE_FORMAT in
   zip)
     TGT="$ARCHIVE.zip"
-    TGT="$(realpath "$TGT")"
-    pushd "$PREFIX"
-    zip -q -r -9 "$TGT" .
-    popd
+    ATGT="$(realpath "$TGT")"
+    pushd "$PREFIX" >/dev/null
+    LEVEL=
+    if release; then
+      LEVEL=-9
+    fi
+    $WRAP zip -q -r $LEVEL "$ATGT" .
+    popd >/dev/null
+    ;;
+  7z)
+    TGT="$ARCHIVE.zip"
+    ATGT="$(realpath "$TGT")"
+    LEVEL=
+    if release; then
+      LEVEL=-mx9
+    fi
+    pushd "$PREFIX" >/dev/null
+    $WRAP 7z $LEVEL a "$ATGT" .
+    popd >/dev/null
     ;;
-  tar.gz|tgz|"")
+  tar.gz|tgz)
     # -h: resolve symlinks
-    tar czf "$ARCHIVE.tar.gz" -h -C "$PREFIX" .
+    TGT="$ARCHIVE.tar.gz"
+    $WRAP tar cf "$ARCHIVE.tar" -h -C "$PREFIX" .
+    LEVEL=
+    if release; then
+      LEVEL=-9
+    fi
+    $WRAP gzip -f $LEVEL "$ARCHIVE.tar"
     ;;
   *)
     echo "unrecognized FSTAR_PACKAGE_FORMAT: $FSTAR_PACKAGE_FORMAT" >&2
     exit 1
     ;;
 esac
+
+if ! [ -f "$TGT" ] ; then
+  echo "error: something seems wrong, archive '$TGT' not found?" >&2
+  exit 1
+fi
+
+# bytes=$(stat -c%s "$TGT")
+# echo "Wrote $TGT" ($bytes bytes)"
+# ^ Does not work in Mac (no -c option for stat)
+
+echo "Wrote $TGT"
+ls -l "$TGT" || true

.scripts/mk-package.sh

@@ -1,14 +1,17 @@
 #!/bin/bash
 
-PREFIX="$(realpath -m "$1")" # -m: leading dirs allowed to not exist
+PREFIX="$1"
+mkdir -p "$PREFIX"
+PREFIX="$(realpath "$PREFIX")"
+
 D="$(dirname "$0")"
 
 mkdir -p "$PREFIX"/lib/fstar
 
 TMP=$(mktemp -d)
 $D/get_fstar_z3.sh --full "$TMP"
 
-pushd "$TMP"
+pushd "$TMP" > /dev/null
 
 inst1 () {
 	TGT="$PREFIX/lib/fstar/$1"
@@ -21,6 +24,6 @@ inst1 ./z3-4.8.5/LICENSE.txt
 inst1 ./z3-4.13.3/bin/z3
 inst1 ./z3-4.13.3/LICENSE.txt
 
-popd
+popd > /dev/null
 
 rm -r "$TMP"

.scripts/package_z3.sh

@@ -8,14 +8,10 @@ if [ $# -ne 2 ]; then
 fi
 
 BROOT="$(realpath "$1")"
-PREFIX="$(realpath -m "$2")" # -m: leading dirs allowed to not exist
 
-if [ -e "${PREFIX}" ]; then
-  echo "Destination directory already exists: ${PREFIX}"
-  exit 1
-fi
-
-mkdir -p "${PREFIX}"
+PREFIX="$2"
+mkdir -p "$PREFIX"
+PREFIX="$(realpath "$PREFIX")"
 
 # Note: we must exclude everything in the Dune build directories, since
 # if some files "vanish" during this copy, rsync will fail (even if
@@ -49,7 +45,14 @@ cp mk/src_package_mk.mk "${PREFIX}/Makefile"
 mkdir "${PREFIX}/mk"
 cp mk/lib.mk "${PREFIX}/mk/lib.mk"
 cp mk/common.mk "${PREFIX}/mk/common.mk"
+cp mk/winwrap.sh "${PREFIX}/mk/winwrap.sh"
 cp -H mk/fstar-12.mk "${PREFIX}/mk/fstar-12.mk"
+cp mk/generic.mk "${PREFIX}/mk/generic.mk"
+mkdir "${PREFIX}/.scripts"
+cp .scripts/bin-install.sh  "${PREFIX}/.scripts"
+cp .scripts/mk-package.sh   "${PREFIX}/.scripts"
+cp .scripts/get_fstar_z3.sh "${PREFIX}/.scripts"
+cp .scripts/package_z3.sh   "${PREFIX}/.scripts"
 
 # Remove extra ML files, rsync has resolved the links
 # into the corresponding files already, and these would be