Check world (build F* and all projects) #13
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: Check world (build F* and all projects) | |
| on: | |
| # push: | |
| workflow_dispatch: | |
| workflow_call: | |
| # TODO: | |
| # Is there a way to set the default container? | |
| # Move to the regular fstar-ci-base too | |
| defaults: | |
| run: | |
| shell: bash | |
| jobs: | |
| build-fstar: | |
| runs-on: ubuntu-latest | |
| container: mtzguido/fstar-base-testing | |
| steps: | |
| - name: Cleanup | |
| run: find . -delete | |
| - run: echo "HOME=/home/opam" >> $GITHUB_ENV | |
| - uses: mtzguido/set-opam-env@master | |
| - name: Checkout | |
| uses: actions/checkout@master | |
| with: | |
| path: FStar/ | |
| - name: Prep | |
| run: | | |
| # In case we edited fstar.opam, install new deps here | |
| # This will most likely fail to like krml below, what's going on? | |
| # opam install --confirm-level=unsafe-yes --deps-only ./FStar/fstar.opam | |
| - name: Build | |
| run: make -C FStar -skj$(nproc) | |
| - uses: mtzguido/gci-upload@master | |
| with: | |
| name: FStar | |
| extra: --exclude=FStar/ocaml/_build | |
| hometag: FSTAR | |
| test-fstar: | |
| runs-on: ubuntu-latest | |
| container: mtzguido/fstar-base-testing | |
| needs: build-fstar | |
| steps: | |
| - name: Cleanup | |
| run: find . -delete | |
| - run: echo "HOME=/home/opam" >> $GITHUB_ENV | |
| - uses: mtzguido/set-opam-env@master | |
| - uses: mtzguido/gci-download@master | |
| with: | |
| name: FStar | |
| - name: Test | |
| run: make -C FStar -skj$(nproc) ci-uregressions | |
| test-fstar-boot: | |
| runs-on: ubuntu-latest | |
| container: mtzguido/fstar-base-testing | |
| # needs: build-fstar | |
| # ^ This does not really depend on the previous job, but this can be | |
| # enabled if we wanted to sequentialize them for whatever reason. | |
| # We start from scratch since we need a git repo to check the | |
| # diff, and that is not contained in the artifact. We could just | |
| # take the ulib checked files from the artifact, if we really wanted | |
| # to, but checking ulib with ADMIT is quite fast anyway. | |
| steps: | |
| - name: Cleanup | |
| run: find . -delete | |
| - run: echo "HOME=/home/opam" >> $GITHUB_ENV | |
| - uses: mtzguido/set-opam-env@master | |
| - uses: actions/checkout@master | |
| with: | |
| path: FStar/ | |
| - name: Bootstrap | |
| run: | | |
| make -C FStar -skj$(nproc) 1 | |
| make -C FStar -skj$(nproc) full-bootstrap ADMIT=1 | |
| - name: Check diff | |
| run: | | |
| cd FStar/ | |
| ./.scripts/check-snapshot-diff.sh | |
| - uses: mtzguido/gci-upload@master | |
| with: | |
| name: FStar-boot | |
| path: FStar | |
| extra: --exclude=FStar/ocaml/_build | |
| hometag: FSTAR | |
| build-pulse: | |
| runs-on: ubuntu-latest | |
| container: mtzguido/fstar-base-testing | |
| needs: | |
| - build-fstar | |
| steps: | |
| - name: Cleanup | |
| run: find . -delete | |
| - run: echo "HOME=/home/opam" >> $GITHUB_ENV | |
| - uses: mtzguido/set-opam-env@master | |
| - uses: mtzguido/gci-download@master | |
| with: | |
| name: FStar | |
| - name: Checkout pulse | |
| uses: actions/checkout@master | |
| with: | |
| path: pulse/ | |
| repository: FStarLang/pulse | |
| - name: Build | |
| run: make -C pulse -skj$(nproc) | |
| - uses: mtzguido/gci-upload@master | |
| with: | |
| name: pulse | |
| hometag: PULSE | |
| test-pulse-boot: | |
| runs-on: ubuntu-latest | |
| container: mtzguido/fstar-base-testing | |
| needs: | |
| - test-fstar-boot | |
| steps: | |
| - name: Cleanup | |
| run: find . -delete | |
| - run: echo "HOME=/home/opam" >> $GITHUB_ENV | |
| - uses: mtzguido/set-opam-env@master | |
| - uses: mtzguido/gci-download@master | |
| with: | |
| name: FStar-boot | |
| - name: Checkout pulse | |
| uses: actions/checkout@master | |
| with: | |
| path: pulse/ | |
| repository: FStarLang/pulse | |
| - name: Build | |
| run: | | |
| # This is similar for 'make full-boot', but does not | |
| # check the library. | |
| make -C pulse/src -skj$(nproc) clean-snapshot | |
| make -C pulse/src -skj$(nproc) extract | |
| make -C pulse/src -skj$(nproc) build | |
| - name: Check diff | |
| run: | | |
| cd pulse/ | |
| ./.scripts/check-snapshot-diff.sh |