From 07fd7ba68e1872b32509fa50aecc73adbf7b66eb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 13 Jan 2025 18:40:21 -0800 Subject: [PATCH 1/2] mk: fixes for src_package in Windows, disabling parallelism --- .scripts/make_fstar_version.sh | 8 +++-- .scripts/src-install.sh | 11 ++++++- mk/src_package_mk.mk | 59 ++++++++++++++++++++-------------- 3 files changed, 50 insertions(+), 28 deletions(-) diff --git a/.scripts/make_fstar_version.sh b/.scripts/make_fstar_version.sh index e47448b6a36..df75bdb6851 100755 --- a/.scripts/make_fstar_version.sh +++ b/.scripts/make_fstar_version.sh @@ -22,13 +22,17 @@ COMPILER="OCaml $(ocamlc -version)" # If a system does not have git, or we are not in a git repo, fallback with "unset" if [[ -z "$FSTAR_COMMIT" ]] ; then FSTAR_COMMIT=$(git describe --match="" --always --abbrev=40 --dirty 2>/dev/null || echo unset) + # NB: ^ has to be in-sync with src-install.sh +fi +if [[ -z "$FSTAR_COMMITDATE" ]] ; then + FSTAR_COMMITDATE=$(git log --pretty=format:%ci -n 1 2>/dev/null || echo unset) + # NB: ^ has to be in-sync with src-install.sh fi -COMMITDATE=$(git log --pretty=format:%ci -n 1 2>/dev/null || echo unset) echo "let dummy () = ();;" echo "FStarC_Options._version := \"$FSTAR_VERSION\";;" echo "FStarC_Options._platform := \"$PLATFORM\";;" echo "FStarC_Options._compiler := \"$COMPILER\";;" # We deliberately use commitdate instead of date, so that rebuilds are no-ops -echo "FStarC_Options._date := \"$COMMITDATE\";;" +echo "FStarC_Options._date := \"$FSTAR_COMMITDATE\";;" echo "FStarC_Options._commit:= \"$FSTAR_COMMIT\";;" diff --git a/.scripts/src-install.sh b/.scripts/src-install.sh index 3b8802e8ef6..a106ae587d5 100755 --- a/.scripts/src-install.sh +++ b/.scripts/src-install.sh @@ -41,7 +41,6 @@ cp version.txt "${PREFIX}" cp -H -r src "${PREFIX}/src" cp .scripts/get_fstar_z3.sh "${PREFIX}/get_fstar_z3.sh" cp fstar.opam "${PREFIX}/fstar.opam" -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" @@ -54,6 +53,16 @@ cp .scripts/mk-package.sh "${PREFIX}/.scripts" cp .scripts/get_fstar_z3.sh "${PREFIX}/.scripts" cp .scripts/package_z3.sh "${PREFIX}/.scripts" +cp mk/src_package_mk.mk "${PREFIX}/Makefile" + +# Make sure the source package has a proper version. +FSTAR_COMMIT=$(git describe --match="" --always --abbrev=40 --dirty 2>/dev/null || echo unset) +FSTAR_COMMITDATE=$(git log --pretty=format:%ci -n 1 2>/dev/null || echo unset) +# NB: ^ has to be in-sync with make_fstar_version.sh +echo "## LINES BELOW ADDED BY src-install.sh" >> "${PREFIX}/Makefile" +echo "export FSTAR_COMMITDATE=$FSTAR_COMMITDATE" >> "${PREFIX}/Makefile" +echo "export FSTAR_COMMIT=$FSTAR_COMMIT" >> "${PREFIX}/Makefile" + # Remove extra ML files, rsync has resolved the links # into the corresponding files already, and these would be # duplicates. diff --git a/mk/src_package_mk.mk b/mk/src_package_mk.mk index 873325aede4..e8073f74fcb 100644 --- a/mk/src_package_mk.mk +++ b/mk/src_package_mk.mk @@ -1,11 +1,7 @@ # This makefile is for OCaml source distributions. # -# FSTAR_DUNE_OPTIONS += --no-print-directory -# FSTAR_DUNE_OPTIONS += --display=quiet -# -# Also note: this Makefile should run in Windows too. Some -# of the $(call cygpath, ..) below are in support of this. Example -# windows error: +# Also note: this Makefile should run in Windows too. Some of the $(call +# cygpath, ..) below are in support of this. Example windows error: # # ... # dune install --root=dune --prefix=/cygdrive/d/a/FStar/FStar/fstar/out @@ -22,14 +18,31 @@ # # I think this is probably a dune bug. +# NOTE: (Guido 2025-01-13) For whatever undebuggable reason, Cygwin make +# (version 4.4.1-1 at least) to (sometimes) freeze , and halt the build. +# Not running this makefile (and sub-makes) in parallel *seems* to help, +# though obviously makes this significantly slower in Windows. +ifeq ($(OS),Windows_NT) +.NOTPARALLEL: +MAYBEJ1=-j1 +else +MAYBEJ1= +endif + include mk/common.mk +FSTAR_DUNE_OPTIONS += --no-print-directory +FSTAR_DUNE_OPTIONS += --display=quiet + FSTAR_DUNE_BUILD_OPTIONS := $(FSTAR_DUNE_OPTIONS) .DEFAULT_GOAL:= all -.PHONY: _force -_force: +.PHONY: .force +.force: +# In some places, we need to compute absolute paths, and in a Cygwin +# enviroment we need Windows-style paths (forward slashes ok, but no +# /cygdrive/). ifeq ($(OS),Windows_NT) cygpath=$(shell cygpath -m "$(abspath $(1))") else @@ -54,19 +67,13 @@ check_lib: install_bin CODEGEN=none \ OUTPUT_DIR=none \ FSTAR_ROOT=$(CURDIR) \ - $(MAKE) -f mk/lib.mk verify - -ifeq ($(OS),Windows_NT) -vv=-v -else -vv= -endif + $(MAKE) -f mk/lib.mk verify $(MAYBEJ1) install_lib: check_lib $(call msg, "INSTALL LIB") @# Install library and its checked files - cp $(vv) -T -H -p -r ulib out/lib/fstar/ulib - cp $(vv) -T -H -p -r ulib.checked out/lib/fstar/ulib.checked + cp -T -H -p -r ulib out/lib/fstar/ulib + cp -T -H -p -r ulib.checked out/lib/fstar/ulib.checked echo 'ulib' > out/lib/fstar/fstar.include echo 'ulib.checked' >> out/lib/fstar/fstar.include @@ -81,19 +88,20 @@ check_fstarc: install_bin TAG=fstarc \ FSTAR_LIB=$(call cygpath,ulib) \ FSTAR_ROOT=$(CURDIR) \ - $(MAKE) -f mk/fstar-12.mk all-checked + $(MAKE) -f mk/fstar-12.mk verify $(MAYBEJ1) + $(call msg, "DONE CHECK FSTARC") install_fstarc: check_fstarc $(call msg, "INSTALL FSTARC") @# Install checked files for FStarC mkdir -p out/lib/fstar/fstarc/ - cp $(vv) -T -H -p -r src out/lib/fstar/fstarc/src - cp $(vv) -T -H -p -r fstarc.checked out/lib/fstar/fstarc/src.checked + cp -T -H -p -r src out/lib/fstar/fstarc/src + cp -T -H -p -r fstarc.checked out/lib/fstar/fstarc/src.checked echo 'src' > out/lib/fstar/fstarc/fstar.include echo 'src.checked' >> out/lib/fstar/fstarc/fstar.include -trim: _force - @echo DUNE CLEAN +trim: .force + $(call msg, "DUNE CLEAN") dune clean $(FSTAR_DUNE_OPTIONS) --root=dune clean: trim @@ -116,6 +124,7 @@ install: install_lib install_fstarc cp -r out/* $(PREFIX) package: - $(MAKE) install PREFIX=fstar - .scripts/bin-install.sh fstar - .scripts/mk-package.sh fstar fstar$(FSTAR_TAG) + mkdir pkgtmp + $(MAKE) install PREFIX=pkgtmp/fstar + .scripts/bin-install.sh pkgtmp/fstar + .scripts/mk-package.sh pkgtmp fstar$(FSTAR_TAG) From a9261414a381628c720d8f273e937d954349fb8d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 13 Jan 2025 18:38:16 -0800 Subject: [PATCH 2/2] actions: building Windows packages, from a src package --- .github/workflows/build-all.yml | 3 + .github/workflows/build-linux.yml | 13 +-- .github/workflows/build-src.yml | 67 ++++++++++++++ .github/workflows/build-windows.yml | 134 ++++++++++++++++++++++++++++ .github/workflows/windows.yml | 28 ------ 5 files changed, 211 insertions(+), 34 deletions(-) create mode 100644 .github/workflows/build-src.yml create mode 100644 .github/workflows/build-windows.yml delete mode 100644 .github/workflows/windows.yml diff --git a/.github/workflows/build-all.yml b/.github/workflows/build-all.yml index 09d68a3c41f..24dc9f8f063 100644 --- a/.github/workflows/build-all.yml +++ b/.github/workflows/build-all.yml @@ -12,3 +12,6 @@ jobs: build-macos: uses: ./.github/workflows/build-macos.yml + + build-windows: + uses: ./.github/workflows/build-windows.yml diff --git a/.github/workflows/build-linux.yml b/.github/workflows/build-linux.yml index da2fc110b31..49a7f84167c 100644 --- a/.github/workflows/build-linux.yml +++ b/.github/workflows/build-linux.yml @@ -48,14 +48,15 @@ jobs: ARCH=$(uname -m) export FSTAR_TAG=-$KERNEL-$ARCH make -skj$(nproc) package - make -skj$(nproc) package-src FSTAR_TAG= - # ^ no tag in source package + # Currently creating the source package in a separate job + # make -skj$(nproc) package-src FSTAR_TAG= + # # ^ no tag in source package - 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 + # - uses: actions/upload-artifact@v4 + # with: + # path: fstar-src.tar.gz + # name: package-src diff --git a/.github/workflows/build-src.yml b/.github/workflows/build-src.yml new file mode 100644 index 00000000000..8a4a4ca6b7d --- /dev/null +++ b/.github/workflows/build-src.yml @@ -0,0 +1,67 @@ +name: Build F* (src) + +on: + workflow_call: + workflow_dispatch: + +defaults: + run: + shell: bash + +jobs: + build-linux: + 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 + id: checkout + + - name: Check cache + id: check-cache + uses: actions/cache/restore@v4 + with: + path: fstar-src.tar.gz + key: FStar-src-${{steps.checkout.outputs.commit}} + + - 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 + echo FSTAR_RELEASE=1 >> $GITHUB_ENV + fi + + # NB: release workflow later adds version number to the name + - name: Build package + if: steps.check-cache.outputs.cache-hit != 'true' + run: | + eval $(opam env) + export FSTAR_TAG= + # ^ no tag in source package + make -skj$(nproc) package-src ADMIT=1 + + - name: Save + if: steps.check-cache.outputs.cache-hit != 'true' + uses: actions/cache/save@v4 + with: + path: fstar-src.tar.gz + key: FStar-src-${{steps.checkout.outputs.commit}} + + - uses: actions/upload-artifact@v4 + with: + path: fstar-src.tar.gz + name: package-src diff --git a/.github/workflows/build-windows.yml b/.github/workflows/build-windows.yml new file mode 100644 index 00000000000..86f6485602e --- /dev/null +++ b/.github/workflows/build-windows.yml @@ -0,0 +1,134 @@ +name: Build F* (Windows) + +# Build F* on Windows +# Note: this workflow is rather messy, prints a bunch of debugging info, +# and relies on a source package generated by a previous (Linux) job. +# Debugging Windows builds is a bit of a nightmare, and can fail in many +# subtle ways. Make sure to test any change thoroughly. +# +# At some point, this should just look exactly like the Linux and macos +# workflows, just running 'make package' in a proper environment, and +# doing a full bootstrapping build. + +on: + workflow_call: + workflow_dispatch: + +defaults: + run: + shell: + bash + +jobs: + # We being from a source package (built in Linux) + build-src: + uses: ./.github/workflows/build-src.yml + + build-windows: + needs: build-src + runs-on: windows-latest + steps: + - uses: cygwin/cygwin-install-action@master + + # Print out some debug info + - name: dbg + continue-on-error: true + run: | + echo 'uname -a' + uname -a || true + echo 'uname -s' + uname -s || true + echo 'uname -m' + uname -m || true + echo env + env || true + echo OS=$OS + which make || true + make --version || true + + - uses: ocaml/setup-ocaml@v3 + with: + ocaml-compiler: 4.14.2 + + # - name: Prepare + # shell: powershell # somehow in bash we fail to build ocamlfind? + # run: | + # ./FStar/.scripts/get_fstar_z3.sh $HOME/bin + # echo "PATH=$HOME/bin:$PATH" >> $GITHUB_ENV + # opam install --deps-only FStar\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 FStar/version.txt)" >> $GITHUB_ENV + fi + + # - name: Build packages + # working-directory: FStar + # run: | + # eval $(opam env) + # KERNEL=Windows_NT + # # $(uname -s) + # # ^ uname-s prints something like CYGWIN_NT-10.0-26100 or MINGW64_NT-10.0-20348 + # ARCH=$(uname -m) + # 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 + # echo ------------------------------------------------- + # make -kj$(nproc) package V=1 + + # - uses: actions/upload-artifact@v4 + # with: + # path: FStar\fstar-Windows_NT-x86_64.tar.gz + # name: fstar-Windows_NT-x86_64.tar.gz + + # Get source package, extract, install its OPAM deps. + - uses: actions/download-artifact@v4 + with: + name: package-src + - run: tar xzf fstar-src.tar.gz + - run: eval $(opam env) && opam install . --deps-only + working-directory: fstar + + # Note: we admit queries here, like the OPAM build does. + - name: Build + run: | + eval $(opam env) + make ADMIT=1 -skj$(nproc) + working-directory: fstar + + - name: Smoke test + continue-on-error: true + run: | + ./out/bin/fstar.exe out/lib/fstar/ulib/Prims.fst -f + echo -e "module A\nopen FStar.Mul\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst + ./out/bin/fstar.exe A.fst + working-directory: fstar + + - name: Make binary package + run: | + eval $(opam env) + KERNEL=Windows_NT + # $(uname -s) + # ^ uname-s prints something like CYGWIN_NT-10.0-26100 or MINGW64_NT-10.0-20348 + ARCH=$(uname -m) + export FSTAR_TAG=-$KERNEL-$ARCH + make package + working-directory: fstar + + - run: find . -name '*.zip' + + - uses: actions/upload-artifact@v4 + if: ${{ always () }} + with: + name: package-win + path: fstar/fstar-*.zip diff --git a/.github/workflows/windows.yml b/.github/workflows/windows.yml deleted file mode 100644 index 959d1521602..00000000000 --- a/.github/workflows/windows.yml +++ /dev/null @@ -1,28 +0,0 @@ -name: FStar Windows Package - -on: - workflow_dispatch: - -jobs: - - build-windows: - - runs-on: [self-hosted, Windows, X64, opam-2-3] - - steps: - - name: Check out repo - uses: actions/checkout@v4 - - - name: Build a package - shell: C:\cygwin64\bin\bash.exe --login '{0}' - run: | - eval $(opam env) && CC=x86_64-w64-mingw32-gcc.exe make -C $GITHUB_WORKSPACE -j package && echo "There is a CR at the end of this line" - - name: Test the package - shell: C:\cygwin64\bin\bash.exe --login '{0}' - run: | - eval $(opam env) && CC=x86_64-w64-mingw32-gcc.exe CI_THREADS=24 $GITHUB_WORKSPACE/.scripts/test_package.sh && echo "There is a CR at the end of this line" - - name: Upload artifact - uses: actions/upload-artifact@v4 - with: - name: fstar-Windows_x86_64.zip - path: src\ocaml-output\fstar.zip