Skip to content

Commit 691c345

Browse files
mtzguidomtzguido
authored
Merge pull request #3721 from mtzguido/release
Bump version number
2 parents 423ca92 + 0fb5b2f commit 691c345

File tree

636 files changed

+32077
-90567
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

636 files changed

+32077
-90567
lines changed

‎.github/workflows/build-windows.yml

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -78,11 +78,11 @@ jobs:
7878
# export FSTAR_TAG=-$KERNEL-$ARCH
7979
# make -kj$(nproc) 0 V=1
8080
# echo -------------------------------------------------
81-
# ./stage0/bin/fstar.exe --version
82-
# ./stage0/bin/fstar.exe --locate
83-
# ./stage0/bin/fstar.exe --locate_lib
84-
# ./stage0/bin/fstar.exe --locate_ocaml
85-
# ./stage0/bin/fstar.exe --include src --debug yes || true
81+
# ./stage0/out/bin/fstar.exe --version
82+
# ./stage0/out/bin/fstar.exe --locate
83+
# ./stage0/out/bin/fstar.exe --locate_lib
84+
# ./stage0/out/bin/fstar.exe --locate_ocaml
85+
# ./stage0/out/bin/fstar.exe --include src --debug yes || true
8686
# echo -------------------------------------------------
8787
# make -kj$(nproc) package V=1
8888

‎Makefile

Lines changed: 5 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -18,14 +18,12 @@ all-packages: package-1 package-2 package-src-1 package-src-2
1818
# to a local build of stage0, to avoid recompiling it every time.
1919
ifneq ($(FSTAR_EXTERNAL_STAGE0),)
2020
FSTAR0_EXE := $(abspath $(FSTAR_EXTERNAL_STAGE0))
21-
_ != mkdir -p stage0/bin
22-
_ != ln -Trsf $(FSTAR0_EXE) stage0/bin/fstar.exe
21+
_ != mkdir -p stage0/out/bin
22+
_ != ln -Trsf $(FSTAR0_EXE) stage0/out/bin/fstar.exe
2323
# ^ Setting this link allows VS code to work seamlessly.
2424
endif
2525

26-
# When stage0 is bumped, use this:
27-
#FSTAR0_EXE ?= stage0/out/bin/fstar.exe
28-
FSTAR0_EXE ?= stage0/bin/fstar.exe
26+
FSTAR0_EXE ?= stage0/out/bin/fstar.exe
2927

3028
# This is hardcoding some dune paths, with internal (non-public) names.
3129
# This is motivated by dune installing packages as a unit, so I could not
@@ -72,11 +70,8 @@ build: 2
7270
0 $(FSTAR0_EXE):
7371
$(call bold_msg, "STAGE 0")
7472
mkdir -p stage0/ulib/.cache # prevent warnings
75-
$(MAKE) -C stage0 fstar
73+
$(MAKE) -C stage0 install_bin # build: only fstar.exe
7674
$(MAKE) -C stage0 trim # We don't need OCaml build files.
77-
# When the stage is bumped, use this:
78-
# $(MAKE) -C stage0 build # build: only fstar.exe
79-
# $(MAKE) -C stage0 trim # We don't need OCaml build files.
8075

8176
.bare1.src.touch: $(FSTAR0_EXE) .force
8277
$(call bold_msg, "EXTRACT", "STAGE 1 FSTARC-BARE")
@@ -435,7 +430,7 @@ ci: .force
435430
save: stage0_new
436431

437432
stage0_new: TO=stage0_new
438-
stage0_new: .stage2.touch
433+
stage0_new: .stage2.src.touch
439434
$(call bold_msg, "SNAPSHOT", "$(TO)")
440435
rm -rf "$(TO)"
441436
.scripts/src-install.sh "stage2" "$(TO)"

‎fstar.opam

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
opam-version: "2.0"
2-
version: "2025.01.06~dev"
2+
version: "2025.02.06~dev"
33
maintainer: "taramana@microsoft.com"
44
authors: "Nik Swamy <nswamy@microsoft.com>,Jonathan Protzenko <protz@microsoft.com>,Tahina Ramananandro <taramana@microsoft.com>"
55
homepage: "http://fstar-lang.org"

‎src/FStarCompiler.fst.config.json

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
{
2-
"fstar_exe": "../stage0/bin/fstar.exe",
2+
"fstar_exe": "../stage0/out/bin/fstar.exe",
33
"options": [
44
"--MLish",
55
"--MLish_effect", "FStarC.Effect",

‎stage0/.fstarlock

Whitespace-only changes.

‎stage0/.gitattributes

Lines changed: 0 additions & 2 deletions
This file was deleted.

‎stage0/.gitignore

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1 @@
1-
# copied from the root
2-
version.txt
3-
/lib
1+
out

‎stage0/.scripts/bin-install.sh

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
#!/bin/bash
2+
3+
# This is called by the Makefile *after* an installation into the
4+
# prefix, so we add the rest of the files that go into a binary package.
5+
6+
set -eu
7+
8+
windows () {
9+
# This seems portable enough and does not trigger an
10+
# undefined variable error (see set -u above) if $OS
11+
# is unset (like in linux/mac). Note: OSX's bash is usually
12+
# old and does not support '[ -v OS ]'.
13+
[[ "${OS:-}" = "Windows_NT" ]]
14+
}
15+
16+
if [ $# -ne 1 ]; then
17+
echo "Usage: $0 <prefix>" >&2
18+
exit 1
19+
fi
20+
21+
PREFIX="$1"
22+
mkdir -p "$PREFIX"
23+
PREFIX="$(realpath "$PREFIX")"
24+
25+
if ! [ -v FSTAR_PACKAGE_Z3 ] || ! [ "$FSTAR_PACKAGE_Z3" = false ]; then
26+
.scripts/package_z3.sh "$PREFIX"
27+
fi
28+
29+
if windows; then
30+
# This dll is needed. It must be installed if we're packaging, as we
31+
# must have run F* already, but it should probably be obtained from
32+
# somewhere else..
33+
LIBGMP=$(which libgmp-10.dll) || echo "error: libgmp-10.dll not found! Carrying on..." >&2
34+
cp "$LIBGMP" "$PREFIX/bin"
35+
fi
36+
37+
# License and extra files. Not there on normal installs, but present in
38+
# package.
39+
cp LICENSE* "$PREFIX"
40+
cp README.md "$PREFIX"
41+
cp INSTALL.md "$PREFIX"
42+
cp version.txt "$PREFIX"
43+
44+
# Save the megabytes! Strip binaries
45+
STRIP=strip
46+
47+
if windows; then
48+
STRIP="$(pwd)/mk/winwrap.sh $STRIP"
49+
fi
50+
51+
$STRIP "$PREFIX"/bin/* || true
52+
$STRIP "$PREFIX"/lib/fstar/z3-*/bin/* || true

‎stage0/.scripts/get_fstar_z3.sh

Lines changed: 146 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,146 @@
1+
#!/usr/bin/env bash
2+
set -euo pipefail
3+
4+
full_install=false
5+
6+
kernel="$(uname -s)"
7+
case "$kernel" in
8+
CYGWIN*) kernel=Windows ;;
9+
esac
10+
11+
arch="$(uname -m)"
12+
case "$arch" in
13+
arm64) arch=aarch64 ;;
14+
esac
15+
16+
release_url=(
17+
"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"
18+
"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"
19+
"Windows-x86_64-4.8.5":"https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-win.zip"
20+
"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"
21+
"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"
22+
"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"
23+
"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"
24+
"Windows-x86_64-4.13.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-x64-win.zip"
25+
)
26+
27+
get_url() {
28+
local key elem
29+
key="$1"
30+
31+
for elem in "${release_url[@]}"; do
32+
if [ "${elem%%:*}" = "$key" ]; then
33+
echo -n "${elem#*:}"
34+
break
35+
fi
36+
done
37+
}
38+
39+
trap "exit 1" HUP INT PIPE QUIT TERM
40+
cleanup() {
41+
if [ -n "${tmp_dir:-}" ]; then
42+
rm -rf "$tmp_dir"
43+
fi
44+
}
45+
trap "cleanup" EXIT
46+
47+
download_z3() {
48+
local url version destination_file_name base_name z3_path
49+
url="$1"
50+
version="$2"
51+
destination_file_name="$3"
52+
53+
if [ -z "${tmp_dir:-}" ]; then
54+
tmp_dir="$(mktemp -d --tmpdir get_fstar_z3.XXXXXXX)"
55+
fi
56+
57+
echo ">>> Downloading Z3 $version from $url ..."
58+
base_name="$(basename "$url")"
59+
60+
z3_path="${base_name%.zip}/bin/z3"
61+
if [ "$kernel" = Windows ]; then z3_path="$z3_path.exe"; fi
62+
63+
pushd "$tmp_dir" > /dev/null
64+
curl -s -L "$url" -o "$base_name"
65+
66+
unzip -q "$base_name" "$z3_path"
67+
popd > /dev/null
68+
install -m0755 "$tmp_dir/$z3_path" "$destination_file_name"
69+
echo ">>> Installed Z3 $version to $destination_file_name"
70+
}
71+
72+
full_install_z3() {
73+
local url version dest_dir base_name
74+
75+
url="$1"
76+
version="$2"
77+
dest_dir="$3"
78+
79+
mkdir -p "$dest_dir/z3-$version"
80+
pushd "$dest_dir/z3-$version" > /dev/null
81+
82+
echo ">>> Downloading Z3 $version from $url ..."
83+
base_name="$(basename "$url")"
84+
curl -s -L "$url" -o "$base_name"
85+
86+
unzip -q "$base_name"
87+
mv "${base_name%.zip}"/* .
88+
rmdir "${base_name%.zip}"
89+
rm "$base_name"
90+
popd > /dev/null
91+
}
92+
93+
usage() {
94+
echo "Usage: get_fstar_z3.sh destination/directory/bin"
95+
exit 1
96+
}
97+
98+
if [ $# -ge 1 ] && [ "$1" == "--full" ]; then
99+
# Passing --full xyz/ will create a tree like
100+
# xyz/z3-4.8.5/bin/z3
101+
# xyz/z3-4.13.3/bin/z3
102+
# (plus all other files in each package). This is used
103+
# for our binary packages which include Z3.
104+
full_install=true;
105+
shift;
106+
fi
107+
108+
if [ $# -ne 1 ]; then
109+
usage
110+
fi
111+
112+
dest_dir="$1"
113+
114+
mkdir -p "$dest_dir"
115+
116+
for z3_ver in 4.8.5 4.13.3; do
117+
destination_file_name="$dest_dir/z3-$z3_ver"
118+
if [ "$kernel" = Windows ]; then destination_file_name="$destination_file_name.exe"; fi
119+
120+
if [ -f "$destination_file_name" ]; then
121+
echo ">>> Z3 $z3_ver already downloaded to $destination_file_name"
122+
else
123+
key="$kernel-$arch-$z3_ver"
124+
125+
case "$key" in
126+
Linux-aarch64-4.8.5)
127+
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."
128+
key="$kernel-x86_64-$z3_ver"
129+
;;
130+
Darwin-aarch64-4.8.5)
131+
echo ">>> Z3 4.8.5 is not available for aarch64, downloading x86_64 version. You need to install Rosetta 2 to execute it."
132+
key="$kernel-x86_64-$z3_ver"
133+
;;
134+
esac
135+
136+
url="$(get_url "$key")"
137+
138+
if [ -z "$url" ]; then
139+
echo ">>> Z3 $z3_ver not available for this architecture, skipping..."
140+
elif $full_install; then
141+
full_install_z3 "$url" "$z3_ver" "$dest_dir"
142+
else
143+
download_z3 "$url" "$z3_ver" "$destination_file_name"
144+
fi
145+
fi
146+
done

‎stage0/.scripts/mk-package.sh

Lines changed: 117 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,117 @@
1+
#!/bin/bash
2+
3+
set -eu
4+
5+
# This will just create a tar.gz or zip out of a directory.
6+
# You may want to look at src-install.sh and bin-install.sh
7+
# that generate the layouts for a source and binary package,
8+
# and are then packaged up with this script.
9+
10+
if [ $# -ne 2 ]; then
11+
exec >&2
12+
echo "usage: $0 <install_root> <package_basename>"
13+
echo "The archive format and command used depends on the system and installed tools,"
14+
echo "see script for details."
15+
echo "Optionally set FSTAR_PACKAGE_FORMAT to: "
16+
echo " - 'zip': create a .zip via 'zip' command"
17+
echo " - '7z': create a .zip via '7z' command"
18+
echo " - 'tar.gz': create a .tar.gz, via calling"
19+
echo "Output filename is <package_basename> + proper extension"
20+
echo "If FSTAR_RELEASE is non-empty, we use maximum compression."
21+
exit 1
22+
fi
23+
24+
PREFIX="$1"
25+
ARCHIVE="$2"
26+
27+
windows () {
28+
# This seems portable enough and does not trigger an
29+
# undefined variable error (see set -u above) if $OS
30+
# is unset (like in linux/mac). Note: OSX's bash is usually
31+
# old and does not support '[ -v OS ]'.
32+
[[ "${OS:-}" = "Windows_NT" ]]
33+
}
34+
35+
release () {
36+
[[ -n "${FSTAR_RELEASE:-}" ]]
37+
}
38+
39+
# Computes a (hopefully) sensible default for the current system
40+
detect_format () {
41+
if windows; then
42+
# Github actions runner do not have 'zip'
43+
if which zip > /dev/null; then
44+
FSTAR_PACKAGE_FORMAT=zip
45+
elif which 7z > /dev/null; then
46+
FSTAR_PACKAGE_FORMAT=7z
47+
else
48+
echo "error: no zip or 7z command found." >&2
49+
exit 1
50+
fi
51+
else
52+
FSTAR_PACKAGE_FORMAT=tar.gz
53+
fi
54+
}
55+
56+
# If unset, pick a default for the system.
57+
if ! [ -v FSTAR_PACKAGE_FORMAT ]; then
58+
detect_format
59+
fi
60+
61+
# Fix for stupid path confustion in windows
62+
if windows; then
63+
WRAP=$(pwd)/mk/winwrap.sh
64+
else
65+
WRAP=
66+
fi
67+
68+
case $FSTAR_PACKAGE_FORMAT in
69+
zip)
70+
TGT="$ARCHIVE.zip"
71+
ATGT="$(realpath "$TGT")"
72+
pushd "$PREFIX" >/dev/null
73+
LEVEL=
74+
if release; then
75+
LEVEL=-9
76+
fi
77+
$WRAP zip -q -r $LEVEL "$ATGT" .
78+
popd >/dev/null
79+
;;
80+
7z)
81+
TGT="$ARCHIVE.zip"
82+
ATGT="$(realpath "$TGT")"
83+
LEVEL=
84+
if release; then
85+
LEVEL=-mx9
86+
fi
87+
pushd "$PREFIX" >/dev/null
88+
$WRAP 7z $LEVEL a "$ATGT" .
89+
popd >/dev/null
90+
;;
91+
tar.gz|tgz)
92+
# -h: resolve symlinks
93+
TGT="$ARCHIVE.tar.gz"
94+
$WRAP tar cf "$ARCHIVE.tar" -h -C "$PREFIX" .
95+
LEVEL=
96+
if release; then
97+
LEVEL=-9
98+
fi
99+
$WRAP gzip -f $LEVEL "$ARCHIVE.tar"
100+
;;
101+
*)
102+
echo "unrecognized FSTAR_PACKAGE_FORMAT: $FSTAR_PACKAGE_FORMAT" >&2
103+
exit 1
104+
;;
105+
esac
106+
107+
if ! [ -f "$TGT" ] ; then
108+
echo "error: something seems wrong, archive '$TGT' not found?" >&2
109+
exit 1
110+
fi
111+
112+
# bytes=$(stat -c%s "$TGT")
113+
# echo "Wrote $TGT" ($bytes bytes)"
114+
# ^ Does not work in Mac (no -c option for stat)
115+
116+
echo "Wrote $TGT"
117+
ls -l "$TGT" || true

0 commit comments

Comments
 (0)