Build everparse package (windows) #15
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Build everparse package (windows) | |
| on: | |
| workflow_dispatch: | |
| inputs: | |
| fstar_repo: | |
| description: F* repository (use org/repo for Github repos) | |
| default: 'FStarLang/FStar' | |
| type: string | |
| required: true | |
| fstar_ref: | |
| description: F* ref (branch, or tag, or commit hash) | |
| default: 'master' | |
| type: string | |
| required: true | |
| karamel_repo: | |
| description: Karamel repository (use org/repo for Github repos) | |
| default: 'FStarLang/karamel' | |
| type: string | |
| required: true | |
| karamel_ref: | |
| description: Karamel ref (branch, or tag, or commit hash) | |
| default: 'master' | |
| type: string | |
| required: true | |
| jobs: | |
| fstar-src: | |
| ## NOTE: This is copied from build-src in the F* repo. | |
| 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 | |
| with: | |
| repository: ${{inputs.fstar_repo}} | |
| ref: ${{inputs.fstar_ref}} | |
| - 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 | |
| if: steps.check-cache.outputs.cache-hit != 'true' | |
| with: | |
| ocaml-compiler: 4.14.2 | |
| - name: Prepare | |
| if: steps.check-cache.outputs.cache-hit != 'true' | |
| run: | | |
| ./.scripts/get_fstar_z3.sh $HOME/bin | |
| echo "PATH=$HOME/bin:$PATH" >> $GITHUB_ENV | |
| opam install --deps-only ./fstar.opam | |
| - name: Set F* version | |
| if: steps.check-cache.outputs.cache-hit != 'true' | |
| run: | | |
| echo FSTAR_VERSION="$(git describe --tags --dirty)" >> $GITHUB_ENV | |
| # 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 | |
| fstar-binary: | |
| runs-on: [self-hosted, windows, X64, opam-2-3] | |
| needs: fstar-src | |
| steps: | |
| - 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" | |
| - uses: actions/download-artifact@v4 | |
| with: | |
| name: package-src | |
| # - name: Check cache | |
| # id: check-cache | |
| # uses: actions/cache/restore@v4 | |
| # with: | |
| # path: fstar.zip | |
| # key: FStar-${{runner.os}}-${{ hashFiles('/fstar-src.tar.gz') }} | |
| - run: cd $GITHUB_WORKSPACE && tar xzf fstar-src.tar.gz && echo "" | |
| # if: steps.check-cache.outputs.cache-hit != 'true' | |
| shell: C:\cygwin64\bin\bash.exe --login '{0}' | |
| - name: Build a package | |
| # if: steps.check-cache.outputs.cache-hit != 'true' | |
| 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 .. && echo "There is a CR at the end of this line" | |
| # - name: Save | |
| # if: steps.check-cache.outputs.cache-hit != 'true' | |
| # uses: actions/cache/save@v4 | |
| # with: | |
| # path: fstar.zip | |
| # key: FStar-${{runner.os}}-${{ hashFiles('/fstar-src.tar.gz') }} | |
| - uses: actions/upload-artifact@v4 | |
| with: | |
| name: fstar-package | |
| path: fstar.zip | |
| build: | |
| runs-on: [self-hosted, windows, X64, opam-2-3] | |
| needs: fstar-binary | |
| steps: | |
| - uses: actions/checkout@master | |
| - uses: actions/checkout@master | |
| with: | |
| path: karamel | |
| repository: ${{inputs.karamel_repo}} | |
| ref: ${{inputs.karamel_ref}} | |
| - uses: actions/download-artifact@v4 | |
| with: | |
| name: fstar-package | |
| - name: Prepare | |
| # opam install --deps-only FStar/fstar.opam | |
| # ^ relying on the fact that F* dependencies are already installed | |
| if: false | |
| # Disabling this, I get | |
| # Error: Package karamel has no version opam. | |
| # but karamel.opam should refer to the file? This also did not | |
| # work with karamel/karamel.opam (without cd'ing). | |
| shell: C:\cygwin64\bin\bash.exe --login '{0}' | |
| run: | | |
| cd $GITHUB_WORKSPACE && eval $(opam env) && cd karamel && sed -i '/"fstar"/d' karamel.opam && opam install --deps-only karamel.opam && opam install hex re sexplib && echo "" | |
| - name: Build package | |
| shell: C:\cygwin64\bin\bash.exe --login '{0}' | |
| run: | | |
| cd $GITHUB_WORKSPACE && eval $(opam env) && CC=x86_64-w64-mingw32-gcc.exe make nuget-noversion -kj$(nproc) && echo "" | |
| - uses: actions/upload-artifact@v4 | |
| with: | |
| include-hidden-files: true | |
| path: | | |
| everparse | |
| name: everparse | |
| - uses: actions/upload-artifact@v4 | |
| with: | |
| path: | | |
| EverParse*.nupkg | |
| name: everparse-nupkg | |
| test: | |
| needs: build | |
| runs-on: windows-latest | |
| steps: | |
| - name: Download and extract artifact | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: everparse | |
| path: ${{ github.workspace }}\test | |
| - name: Check out repo | |
| uses: actions/checkout@v4 | |
| with: | |
| sparse-checkout: src\3d\tests | |
| path: ${{ github.workspace }}\everparse | |
| - name: Test EverParse | |
| shell: cmd | |
| run: | | |
| ${{ github.workspace }}\test\everparse.cmd ${{ github.workspace }}\everparse\src\3d\tests\Arithmetic.3d ${{ github.workspace }}\everparse\src\3d\tests\FieldDependence0.3d && ${{ github.workspace }}\test\everparse.cmd ${{ github.workspace }}\everparse\src\3d\tests\Comments.3d && ${{ github.workspace }}\test\everparse.cmd --check_hashes inplace ${{ github.workspace }}\everparse\src\3d\tests\Comments.3d |