diff --git a/.github/workflows/build-all.yml b/.github/workflows/build-all.yml index 68739869a62..fd17978d9f6 100644 --- a/.github/workflows/build-all.yml +++ b/.github/workflows/build-all.yml @@ -5,15 +5,15 @@ on: workflow_dispatch: jobs: - # Disable when Windows is reenabled. - build-src: - uses: ./.github/workflows/build-src.yml + # Windows build call this as a substep + # 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: - # uses: ./.github/workflows/build-windows.yml + 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 new file mode 100644 index 00000000000..9d7f9439d38 --- /dev/null +++ b/.github/workflows/build-windows-selfhosted.yml @@ -0,0 +1,74 @@ +name: Build F* (Windows, self-hosted) + +on: + workflow_call: + workflow_dispatch: + +jobs: + # We begin from a source package (built in Linux) + build-src: + uses: ./.github/workflows/build-src.yml + + 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. + # 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 + # 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..eec72483948 100644 --- a/.github/workflows/build-windows.yml +++ b/.github/workflows/build-windows.yml @@ -20,11 +20,11 @@ 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 - build-windows: + build: needs: build-src runs-on: windows-latest steps: 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: 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 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 diff --git a/mk/src_package_mk.mk b/mk/src_package_mk.mk index e8073f74fcb..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 @@ -106,8 +95,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 +113,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) 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