Bump version number

.github/workflows/build-windows.yml

@@ -78,11 +78,11 @@ jobs:
       #     export FSTAR_TAG=-$KERNEL-$ARCH
       #     make -kj$(nproc) 0 V=1
       #     echo -------------------------------------------------
-      #     ./stage0/bin/fstar.exe --version
-      #     ./stage0/bin/fstar.exe --locate
-      #     ./stage0/bin/fstar.exe --locate_lib
-      #     ./stage0/bin/fstar.exe --locate_ocaml
-      #     ./stage0/bin/fstar.exe --include src --debug yes || true
+      #     ./stage0/out/bin/fstar.exe --version
+      #     ./stage0/out/bin/fstar.exe --locate
+      #     ./stage0/out/bin/fstar.exe --locate_lib
+      #     ./stage0/out/bin/fstar.exe --locate_ocaml
+      #     ./stage0/out/bin/fstar.exe --include src --debug yes || true
       #     echo -------------------------------------------------
       #     make -kj$(nproc) package V=1
 

Makefile

@@ -18,14 +18,12 @@ all-packages: package-1 package-2 package-src-1 package-src-2
 # to a local build of stage0, to avoid recompiling it every time.
 ifneq ($(FSTAR_EXTERNAL_STAGE0),)
 FSTAR0_EXE := $(abspath $(FSTAR_EXTERNAL_STAGE0))
-_ != mkdir -p stage0/bin
-_ != ln -Trsf $(FSTAR0_EXE) stage0/bin/fstar.exe
+_ != mkdir -p stage0/out/bin
+_ != ln -Trsf $(FSTAR0_EXE) stage0/out/bin/fstar.exe
 # ^ Setting this link allows VS code to work seamlessly.
 endif
 
-# When stage0 is bumped, use this:
-#FSTAR0_EXE ?= stage0/out/bin/fstar.exe
-FSTAR0_EXE ?= stage0/bin/fstar.exe
+FSTAR0_EXE ?= stage0/out/bin/fstar.exe
 
 # This is hardcoding some dune paths, with internal (non-public) names.
 # This is motivated by dune installing packages as a unit, so I could not
@@ -72,11 +70,8 @@ build: 2
 0 $(FSTAR0_EXE):
 	$(call bold_msg, "STAGE 0")
 	mkdir -p stage0/ulib/.cache # prevent warnings
-	$(MAKE) -C stage0 fstar
+	$(MAKE) -C stage0 install_bin # build: only fstar.exe
 	$(MAKE) -C stage0 trim # We don't need OCaml build files.
-	# When the stage is bumped, use this:
-	# $(MAKE) -C stage0 build # build: only fstar.exe
-	# $(MAKE) -C stage0 trim # We don't need OCaml build files.
 
 .bare1.src.touch: $(FSTAR0_EXE) .force
 	$(call bold_msg, "EXTRACT", "STAGE 1 FSTARC-BARE")
@@ -435,7 +430,7 @@ ci: .force
 save: stage0_new
 
 stage0_new: TO=stage0_new
-stage0_new: .stage2.touch
+stage0_new: .stage2.src.touch
 	$(call bold_msg, "SNAPSHOT", "$(TO)")
 	rm -rf "$(TO)"
 	.scripts/src-install.sh "stage2" "$(TO)"

fstar.opam

@@ -1,5 +1,5 @@
 opam-version: "2.0"
-version: "2025.01.06~dev"
+version: "2025.02.06~dev"
 maintainer: "[email protected]"
 authors: "Nik Swamy <[email protected]>,Jonathan Protzenko <[email protected]>,Tahina Ramananandro <[email protected]>"
 homepage: "http://fstar-lang.org"

src/FStarCompiler.fst.config.json

@@ -1,5 +1,5 @@
 {
-  "fstar_exe": "../stage0/bin/fstar.exe",
+  "fstar_exe": "../stage0/out/bin/fstar.exe",
   "options": [
     "--MLish",
     "--MLish_effect", "FStarC.Effect",

stage0/.gitignore

@@ -1,3 +1 @@
-# copied from the root
-version.txt
-/lib
+out

stage0/.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

stage0/.scripts/get_fstar_z3.sh

@@ -0,0 +1,146 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+full_install=false
+
+kernel="$(uname -s)"
+case "$kernel" in
+  CYGWIN*) kernel=Windows ;;
+esac
+
+arch="$(uname -m)"
+case "$arch" in
+  arm64) arch=aarch64 ;;
+esac
+
+release_url=(
+  "Linux-x86_64-4.8.5":"https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-ubuntu-16.04.zip"
+  "Darwin-x86_64-4.8.5":"https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-osx-10.14.2.zip"
+  "Windows-x86_64-4.8.5":"https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-win.zip"
+  "Linux-x86_64-4.13.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-x64-glibc-2.35.zip"
+  "Linux-aarch64-4.13.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-arm64-glibc-2.34.zip"
+  "Darwin-x86_64-4.13.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-x64-osx-13.7.zip"
+  "Darwin-aarch64-4.13.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-arm64-osx-13.7.zip"
+  "Windows-x86_64-4.13.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-x64-win.zip"
+)
+
+get_url() {
+  local key elem
+  key="$1"
+
+  for elem in "${release_url[@]}"; do
+    if [ "${elem%%:*}" = "$key" ]; then
+      echo -n "${elem#*:}"
+      break
+    fi
+  done
+}
+
+trap "exit 1" HUP INT PIPE QUIT TERM
+cleanup() {
+  if [ -n "${tmp_dir:-}" ]; then
+    rm -rf "$tmp_dir"
+  fi
+}
+trap "cleanup" EXIT
+
+download_z3() {
+  local url version destination_file_name base_name z3_path
+  url="$1"
+  version="$2"
+  destination_file_name="$3"
+
+  if [ -z "${tmp_dir:-}" ]; then
+    tmp_dir="$(mktemp -d --tmpdir get_fstar_z3.XXXXXXX)"
+  fi
+
+  echo ">>> Downloading Z3 $version from $url ..."
+  base_name="$(basename "$url")"
+
+  z3_path="${base_name%.zip}/bin/z3"
+  if [ "$kernel" = Windows ]; then z3_path="$z3_path.exe"; fi
+
+  pushd "$tmp_dir" > /dev/null
+  curl -s -L "$url" -o "$base_name"
+
+  unzip -q "$base_name" "$z3_path"
+  popd > /dev/null
+  install -m0755 "$tmp_dir/$z3_path" "$destination_file_name"
+  echo ">>> Installed Z3 $version to $destination_file_name"
+}
+
+full_install_z3() {
+  local url version dest_dir base_name
+
+  url="$1"
+  version="$2"
+  dest_dir="$3"
+
+  mkdir -p "$dest_dir/z3-$version"
+  pushd "$dest_dir/z3-$version" > /dev/null
+
+  echo ">>> Downloading Z3 $version from $url ..."
+  base_name="$(basename "$url")"
+  curl -s -L "$url" -o "$base_name"
+
+  unzip -q "$base_name"
+  mv "${base_name%.zip}"/* .
+  rmdir "${base_name%.zip}"
+  rm "$base_name"
+  popd > /dev/null
+}
+
+usage() {
+  echo "Usage: get_fstar_z3.sh destination/directory/bin"
+  exit 1
+}
+
+if [ $# -ge 1 ] && [ "$1" == "--full" ]; then
+  # Passing --full xyz/ will create a tree like
+  #  xyz/z3-4.8.5/bin/z3
+  #  xyz/z3-4.13.3/bin/z3
+  # (plus all other files in each package). This is used
+  # for our binary packages which include Z3.
+  full_install=true;
+  shift;
+fi
+
+if [ $# -ne 1 ]; then
+  usage
+fi
+
+dest_dir="$1"
+
+mkdir -p "$dest_dir"
+
+for z3_ver in 4.8.5 4.13.3; do
+  destination_file_name="$dest_dir/z3-$z3_ver"
+  if [ "$kernel" = Windows ]; then destination_file_name="$destination_file_name.exe"; fi
+
+  if [ -f "$destination_file_name" ]; then
+    echo ">>> Z3 $z3_ver already downloaded to $destination_file_name"
+  else
+    key="$kernel-$arch-$z3_ver"
+
+    case "$key" in
+      Linux-aarch64-4.8.5)
+        echo ">>> Z3 4.8.5 is not available for aarch64, downloading x86_64 version.  You need to install qemu-user (and shared libraries) to execute it."
+        key="$kernel-x86_64-$z3_ver"
+        ;;
+      Darwin-aarch64-4.8.5)
+        echo ">>> Z3 4.8.5 is not available for aarch64, downloading x86_64 version.  You need to install Rosetta 2 to execute it."
+        key="$kernel-x86_64-$z3_ver"
+        ;;
+    esac
+
+    url="$(get_url "$key")"
+
+    if [ -z "$url" ]; then
+      echo ">>> Z3 $z3_ver not available for this architecture, skipping..."
+    elif $full_install; then
+      full_install_z3 "$url" "$z3_ver" "$dest_dir"
+    else
+      download_z3 "$url" "$z3_ver" "$destination_file_name"
+    fi
+  fi
+done

stage0/.scripts/mk-package.sh

@@ -0,0 +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
+  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"
+    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)
+    # -h: resolve symlinks
+    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