From cbb511a9135a387616181c4a4afa339b308602c6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 16 Jan 2025 21:38:08 -0800 Subject: [PATCH 1/8] ci: ignore branches beginning with _ --- .github/workflows/ci.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index e51bb02926a..53992ea86d0 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -2,6 +2,8 @@ name: CI on: push: + branches-ignore: + - _** pull_request: workflow_dispatch: merge_group: From 35859c5b55caef11e2ecc5691b890038552a22f6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 15 Jan 2025 15:02:08 -0800 Subject: [PATCH 2/8] FStar_String: move to new Batteries {uppercase,lowercase}_ascii This patch got mistakenly dropped after the new build. --- ulib/ml/app/FStar_String.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ulib/ml/app/FStar_String.ml b/ulib/ml/app/FStar_String.ml index 45c7ba41578..9dcff4a94df 100644 --- a/ulib/ml/app/FStar_String.ml +++ b/ulib/ml/app/FStar_String.ml @@ -29,8 +29,8 @@ let get s i = BatUChar.code (BatUTF8.get s (Z.to_int i)) let collect f s = let r = ref "" in BatUTF8.iter (fun c -> r := !r ^ f (BatUChar.code c)) s; !r -let lowercase = BatString.lowercase -let uppercase = BatString.uppercase +let lowercase = BatString.lowercase_ascii +let uppercase = BatString.uppercase_ascii let escaped = BatString.escaped let index = get exception Found of int From 9bf590ebfe582f881407c71ace55b8af5454f503 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 15 Jan 2025 22:00:31 -0800 Subject: [PATCH 3/8] package_z3: ship DLLs in Windows --- .scripts/package_z3.sh | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/.scripts/package_z3.sh b/.scripts/package_z3.sh index f08150d9138..64f911921fd 100755 --- a/.scripts/package_z3.sh +++ b/.scripts/package_z3.sh @@ -19,10 +19,14 @@ inst1 () { cp "$1" "$TGT" } -inst1 ./z3-4.8.5/bin/z3 -inst1 ./z3-4.8.5/LICENSE.txt -inst1 ./z3-4.13.3/bin/z3 -inst1 ./z3-4.13.3/LICENSE.txt +for dir in z3-4.8.5 z3-4.13.3; do + inst1 ./$dir/bin/z3 + inst1 ./$dir/LICENSE.txt + for dll in ./$dir/bin/*dll; do + # Needed for Windows packages. + inst1 "$dll" + done +done popd > /dev/null From 1c37205d52f7c25ec4699c6b7e55bcf6a199f65d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 15 Jan 2025 22:42:44 -0800 Subject: [PATCH 4/8] src_package_mk: fix clean rule --- mk/src_package_mk.mk | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/mk/src_package_mk.mk b/mk/src_package_mk.mk index e8073f74fcb..be6b754e2c9 100644 --- a/mk/src_package_mk.mk +++ b/mk/src_package_mk.mk @@ -106,8 +106,8 @@ trim: .force clean: trim rm -rf $(CURDIR)/out - rm -r ulib.checked - rm -r fstarc.checked + rm -rf ulib.checked + rm -rf fstarc.checked all: install_lib install_fstarc @@ -124,7 +124,8 @@ install: install_lib install_fstarc cp -r out/* $(PREFIX) package: - mkdir pkgtmp + rm -rf pkgtmp + mkdir -p pkgtmp $(MAKE) install PREFIX=pkgtmp/fstar .scripts/bin-install.sh pkgtmp/fstar .scripts/mk-package.sh pkgtmp fstar$(FSTAR_TAG) From e3342c8708ad2b6496c4209a3faa4cd3c4db14b0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 16 Jan 2025 21:34:42 -0800 Subject: [PATCH 5/8] src-install.sh: propagating version into src package --- .scripts/src-install.sh | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.scripts/src-install.sh b/.scripts/src-install.sh index a106ae587d5..57d2d7a52f1 100755 --- a/.scripts/src-install.sh +++ b/.scripts/src-install.sh @@ -62,6 +62,9 @@ FSTAR_COMMITDATE=$(git log --pretty=format:%ci -n 1 2>/dev/null || echo unset) 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" +if [[ -n "${FSTAR_VERSION:-}" ]]; then + echo "export FSTAR_VERSION=$FSTAR_VERSION" >> "${PREFIX}/Makefile" +fi # Remove extra ML files, rsync has resolved the links # into the corresponding files already, and these would be From d87742c17b42be6f99dcee6605ebd806753bde84 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 15 Jan 2025 10:41:27 -0800 Subject: [PATCH 6/8] Restoring self-hosted windows build --- .github/workflows/build-all.yml | 10 +-- .../workflows/build-windows-selfhosted.yml | 75 +++++++++++++++++++ .github/workflows/build-windows.yml | 2 +- 3 files changed, 81 insertions(+), 6 deletions(-) create mode 100644 .github/workflows/build-windows-selfhosted.yml diff --git a/.github/workflows/build-all.yml b/.github/workflows/build-all.yml index 68739869a62..27dbfe5ab47 100644 --- a/.github/workflows/build-all.yml +++ b/.github/workflows/build-all.yml @@ -5,9 +5,9 @@ on: workflow_dispatch: jobs: - # Disable when Windows is reenabled. - build-src: - uses: ./.github/workflows/build-src.yml + # Windows build call this as a substep + # build-src: + # uses: ./.github/workflows/build-src.yml build-linux: uses: ./.github/workflows/build-linux.yml @@ -15,5 +15,5 @@ jobs: build-macos: uses: ./.github/workflows/build-macos.yml - # build-windows: - # uses: ./.github/workflows/build-windows.yml + build-windows: + uses: ./.github/workflows/build-windows-selfhosted.yml diff --git a/.github/workflows/build-windows-selfhosted.yml b/.github/workflows/build-windows-selfhosted.yml new file mode 100644 index 00000000000..ed46a954904 --- /dev/null +++ b/.github/workflows/build-windows-selfhosted.yml @@ -0,0 +1,75 @@ +name: Build F* (Windows, self-hosted) + +on: + workflow_call: + workflow_dispatch: + push: + +jobs: + # We begin from a source package (built in Linux) + build-src: + uses: ./.github/workflows/build-src.yml + + build-windows: + needs: build-src + runs-on: [self-hosted, Windows, X64, opam-2-3] + # NOTE: no setup, the self-hosted runner already has all that is needed. + # This workflow also has many weird restrictions like + # having to set cygwin bash, cd into $GITHUB_WORKSPACE, and keep + # shell commands to a single line. + steps: + - name: test + shell: C:\cygwin64\bin\bash.exe --login '{0}' + run: echo "GITHUB_WORKSPACE=$GITHUB_WORKSPACE" + + - name: clean + shell: C:\cygwin64\bin\bash.exe --login '{0}' + run: cd $GITHUB_WORKSPACE/ && rm -rf * && echo "There is a CR at the end of this line" + # ^ clean the workspace + + - uses: actions/download-artifact@v4 + with: + name: package-src + - run: cd $GITHUB_WORKSPACE && tar xzf fstar-src.tar.gz + shell: C:\cygwin64\bin\bash.exe --login '{0}' + + # DO NOT DO THIS. These variables will be lost since bash will + # not look at the environment of the calling cmd shell. + # - name: Prepare environment + # shell: C:\cygwin64\bin\bash.exe --login '{0}' + # run: | + # echo "CC=x86_64-w64-mingw32-gcc.exe" >> $GITHUB_ENV + # echo "FSTAR_DUNE_OPTIONS=-j1" >> $GITHUB_ENV + # echo "DUNE_CONFIG__BACKGROUND_SANDBOXES=disabled" >> $GITHUB_ENV + # ^ Related issues: + # https://github.com/ocaml/dune/issues/2324 + # https://github.com/ocaml/dune/issues/10076 + + - name: Build a package + shell: C:\cygwin64\bin\bash.exe --login '{0}' + run: | + cd $GITHUB_WORKSPACE && cd fstar && eval $(opam env) && make clean && CC=x86_64-w64-mingw32-gcc.exe DUNE_CONFIG__BACKGROUND_SANDBOXES=disabled make -j$(nproc) package V=1 ADMIT=1 && mv fstar.zip fstar-Windows_NT-x86_64.zip && echo "There is a CR at the end of this line" + + - name: Upload artifact + uses: actions/upload-artifact@v4 + with: + path: fstar/fstar*.zip + name: package-win + + binary-smoke: + needs: build-windows + # This is a cloud job. + runs-on: windows-latest + steps: + - name: Get package + uses: actions/download-artifact@v4 + with: + name: package-win + + - run: unzip fstar*.zip + shell: bash + + - name: Smoke test + working-directory: fstar + run: | + ./bin/fstar.exe lib/fstar/ulib/Prims.fst -f -d diff --git a/.github/workflows/build-windows.yml b/.github/workflows/build-windows.yml index 86f6485602e..6d227606d37 100644 --- a/.github/workflows/build-windows.yml +++ b/.github/workflows/build-windows.yml @@ -20,7 +20,7 @@ defaults: bash jobs: - # We being from a source package (built in Linux) + # We begin from a source package (built in Linux) build-src: uses: ./.github/workflows/build-src.yml From 74c6a89dc34a39fd77ed1123b0d1630df9c6ff23 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 16 Jan 2025 21:42:53 -0800 Subject: [PATCH 7/8] workflows: tweaking some jobs names --- .github/workflows/build-all.yml | 8 ++++---- .github/workflows/build-linux.yml | 2 +- .github/workflows/build-macos.yml | 2 +- .github/workflows/build-src.yml | 2 +- .github/workflows/build-windows-selfhosted.yml | 5 ++--- .github/workflows/build-windows.yml | 2 +- 6 files changed, 10 insertions(+), 11 deletions(-) diff --git a/.github/workflows/build-all.yml b/.github/workflows/build-all.yml index 27dbfe5ab47..fd17978d9f6 100644 --- a/.github/workflows/build-all.yml +++ b/.github/workflows/build-all.yml @@ -6,14 +6,14 @@ on: jobs: # Windows build call this as a substep - # build-src: + # src: # uses: ./.github/workflows/build-src.yml - build-linux: + linux: uses: ./.github/workflows/build-linux.yml - build-macos: + macos: uses: ./.github/workflows/build-macos.yml - build-windows: + windows: uses: ./.github/workflows/build-windows-selfhosted.yml diff --git a/.github/workflows/build-linux.yml b/.github/workflows/build-linux.yml index 49a7f84167c..e1bd9192ddd 100644 --- a/.github/workflows/build-linux.yml +++ b/.github/workflows/build-linux.yml @@ -12,7 +12,7 @@ defaults: shell: bash jobs: - build-linux: + build: runs-on: ubuntu-22.04 # We prefer slightly older Ubuntu so we get binaries that work on # all more recent versions. diff --git a/.github/workflows/build-macos.yml b/.github/workflows/build-macos.yml index c943f9995f2..9049c4ac502 100644 --- a/.github/workflows/build-macos.yml +++ b/.github/workflows/build-macos.yml @@ -5,7 +5,7 @@ on: workflow_call: jobs: - build-macos: + build: runs-on: macos-latest steps: - uses: actions/checkout@master diff --git a/.github/workflows/build-src.yml b/.github/workflows/build-src.yml index 8a4a4ca6b7d..2341616e2dc 100644 --- a/.github/workflows/build-src.yml +++ b/.github/workflows/build-src.yml @@ -9,7 +9,7 @@ defaults: shell: bash jobs: - build-linux: + build: runs-on: ubuntu-22.04 # We prefer slightly older Ubuntu so we get binaries that work on # all more recent versions. diff --git a/.github/workflows/build-windows-selfhosted.yml b/.github/workflows/build-windows-selfhosted.yml index ed46a954904..9d7f9439d38 100644 --- a/.github/workflows/build-windows-selfhosted.yml +++ b/.github/workflows/build-windows-selfhosted.yml @@ -3,14 +3,13 @@ name: Build F* (Windows, self-hosted) on: workflow_call: workflow_dispatch: - push: jobs: # We begin from a source package (built in Linux) build-src: uses: ./.github/workflows/build-src.yml - build-windows: + build: needs: build-src runs-on: [self-hosted, Windows, X64, opam-2-3] # NOTE: no setup, the self-hosted runner already has all that is needed. @@ -57,7 +56,7 @@ jobs: name: package-win binary-smoke: - needs: build-windows + needs: build # This is a cloud job. runs-on: windows-latest steps: diff --git a/.github/workflows/build-windows.yml b/.github/workflows/build-windows.yml index 6d227606d37..eec72483948 100644 --- a/.github/workflows/build-windows.yml +++ b/.github/workflows/build-windows.yml @@ -24,7 +24,7 @@ jobs: build-src: uses: ./.github/workflows/build-src.yml - build-windows: + build: needs: build-src runs-on: windows-latest steps: From b9000bb5b9c92183f17fe933c208969960e146c1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 16 Jan 2025 22:38:28 -0800 Subject: [PATCH 8/8] src package: restore parallelism in Windows --- mk/src_package_mk.mk | 15 ++------------- 1 file changed, 2 insertions(+), 13 deletions(-) diff --git a/mk/src_package_mk.mk b/mk/src_package_mk.mk index be6b754e2c9..260a3467d7e 100644 --- a/mk/src_package_mk.mk +++ b/mk/src_package_mk.mk @@ -18,17 +18,6 @@ # # 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 @@ -67,7 +56,7 @@ check_lib: install_bin CODEGEN=none \ OUTPUT_DIR=none \ FSTAR_ROOT=$(CURDIR) \ - $(MAKE) -f mk/lib.mk verify $(MAYBEJ1) + $(MAKE) -f mk/lib.mk verify install_lib: check_lib $(call msg, "INSTALL LIB") @@ -88,7 +77,7 @@ check_fstarc: install_bin TAG=fstarc \ FSTAR_LIB=$(call cygpath,ulib) \ FSTAR_ROOT=$(CURDIR) \ - $(MAKE) -f mk/fstar-12.mk verify $(MAYBEJ1) + $(MAKE) -f mk/fstar-12.mk verify $(call msg, "DONE CHECK FSTARC") install_fstarc: check_fstarc