Skip to content

Commit

Permalink
Restoring self-hosted windows build
Browse files Browse the repository at this point in the history
  • Loading branch information
mtzguido committed Jan 16, 2025
1 parent d4078df commit 2472f8b
Show file tree
Hide file tree
Showing 4 changed files with 101 additions and 7 deletions.
91 changes: 91 additions & 0 deletions .github/workflows/build-windows-selfhosted.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,91 @@
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: clean
shell: C:\cygwin64\bin\bash.exe --login '{0}'
run: cd $GITHUB_WORKSPACE && ls -lR && rm -vrf fstar && echo "There is a CR at the end of this line"
# ^ remove the directory where the package extracts to and builds,
# all files from previous runs remain the runner's working directory
# otherwise.

- 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}'

- name: Set version
shell: C:\cygwin64\bin\bash.exe --login '{0}'
run: |
# Setting FSTAR_VERSION for nightly and release builds. If unset,
# we use $(version.txt)~dev. Setting it avoids the ~dev.
cd $GITHUB_WORKSPACE && 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; echo FSTAR_RELEASE=1 >> $GITHUB_ENV; fi && echo "There is a CR at the end of this line"
- 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 && 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"
# paranoid make clean above, seeing a bunch of these non predictably:
# File "libapp/dune", line 18, characters 13-56:
# 18 | (preprocess (pps ppx_deriving.show ppx_deriving_yojson))
# ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
# Error: failed to delete sandbox in
# _build/.sandbox/e99d5dd0c933464aff5f4e9946b620a8)

# - name: Test the package
# shell: C:\cygwin64\bin\bash.exe --login '{0}'
# run: |
# cd $GITHUB_WORKSPACE && cd fstar && eval $(opam env) && export CC=x86_64-w64-mingw32-gcc.exe && export CI_THREADS=$(nproc) && .scripts/test_package.sh && 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
echo -e "module A\nopen FStar.Mul\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst
./bin/fstar.exe A.fst -d
2 changes: 2 additions & 0 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@ name: CI

on:
push:
branches-ignore:
- _**
pull_request:
workflow_dispatch:
merge_group:
Expand Down
14 changes: 8 additions & 6 deletions mk/src_package_mk.mk
Original file line number Diff line number Diff line change
Expand Up @@ -22,12 +22,14 @@
# (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
# LATER EDIT: For the self-hosted runner, this does not seem to be a problem,
# so do not restrict parallelism.
# ifeq ($(OS),Windows_NT)
# .NOTPARALLEL:
# MAYBEJ1=-j1
# else
# MAYBEJ1=
# endif

include mk/common.mk

Expand Down
1 change: 0 additions & 1 deletion mk/stage0.mk
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
# This file is used (or created) by the bring-stage0 rule in the toplevel Makefile

include $(FSTAR_ROOT)/mk/common.mk

Expand Down

0 comments on commit 2472f8b

Please sign in to comment.