Erase functions to functions instead of unit. #1
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: F* CI | |
| on: | |
| push: | |
| workflow_dispatch: | |
| workflow_call: | |
| defaults: | |
| run: | |
| shell: bash | |
| jobs: | |
| build: | |
| # Build an F* binary package: a fully-bootstrapped stage 2 compiler, | |
| # with its plugins, a fully checked library (i.e. with .checked) | |
| # files and compiled versions of fstar_lib and fstar_plugin_lib. | |
| # Also, we build a full stage 1 compiler and its libraries, and | |
| # make all possible artifacts. | |
| runs-on: ubuntu-latest | |
| container: mtzguido/dev-base | |
| steps: | |
| - name: Cleanup | |
| run: find . -delete | |
| - run: echo "HOME=/home/user" >> $GITHUB_ENV | |
| - uses: mtzguido/set-opam-env@master | |
| - name: Checkout | |
| uses: actions/checkout@master | |
| - name: Produce all artifacts | |
| run: make -skj$(nproc) all-packages FSTAR_VERSION=ci | |
| - uses: actions/upload-artifact@v4 | |
| with: | |
| path: fstar-ci.tar.gz | |
| name: fstar-ci.tar.gz | |
| retention-days: 3 | |
| - uses: actions/upload-artifact@v4 | |
| with: | |
| path: fstar-ci-stage1.tar.gz | |
| name: fstar-ci-stage1.tar.gz | |
| retention-days: 3 | |
| - uses: actions/upload-artifact@v4 | |
| with: | |
| path: fstar-ci-src.tar.gz | |
| name: fstar-ci-src.tar.gz | |
| retention-days: 3 | |
| - uses: actions/upload-artifact@v4 | |
| with: | |
| path: fstar-ci-stage1-src.tar.gz | |
| name: fstar-ci-stage1-src.tar.gz | |
| retention-days: 3 | |
| # FIXME: Ideally, we could upload the artifacts as soon as each of | |
| # them is created, and start the subsequent jobs at that instant too. | |
| # Is that even doable...? | |
| check-friends: | |
| needs: build | |
| name: friends | |
| uses: ./.github/workflows/check-friends.yml | |
| # This checks that the stage3 extracted fstarc matches exactly with stage2. | |
| # There is some overlap with the job above, but the testing jobs do not | |
| # need this bit at all and we have plenty of parallelism for now... so just | |
| # spawn another one. | |
| check-stage3-diff: | |
| runs-on: ubuntu-latest | |
| container: mtzguido/dev-base | |
| steps: | |
| - name: Cleanup | |
| run: find . -delete | |
| - run: echo "HOME=/home/user" >> $GITHUB_ENV | |
| - uses: mtzguido/set-opam-env@master | |
| - name: Checkout | |
| uses: actions/checkout@master | |
| - name: Check for a stage 3 diff | |
| run: make -skj$(nproc) stage3-diff | |
| # Download the stage2 binary package from the previous job and run the tests | |
| # in the repo. This makes sure that the tests do not depend on some | |
| # random internal state of the repo, but only on out/. | |
| # | |
| # We could be paranoid and rm -rf ulib too, it should not make a difference. | |
| # | |
| # We also run all tests over the stage 1 compiler. They should all pass, | |
| # just like for stage2. The compiler used to build fstar.exe itself | |
| # should not matter. | |
| test-local: | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| pak: | |
| - fstar-ci.tar.gz | |
| - fstar-ci-stage1.tar.gz | |
| needs: build | |
| runs-on: ubuntu-latest | |
| container: mtzguido/dev-base | |
| steps: | |
| - name: Cleanup | |
| run: find . -delete | |
| - run: echo "HOME=/home/user" >> $GITHUB_ENV | |
| - uses: mtzguido/set-opam-env@master | |
| - name: Checkout | |
| uses: actions/checkout@master | |
| - name: Get fstar package | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: ${{ matrix.pak }} | |
| - name: Set up package locally | |
| run: mkdir -p out && tar xzf ${{ matrix.pak }} -C out | |
| - name: Run tests | |
| run: make -skj$(nproc) test | |
| binary-smoke: | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| pak: | |
| - fstar-ci.tar.gz | |
| - fstar-ci-stage1.tar.gz | |
| os: | |
| # - ubuntu-20.04 | |
| # - ubuntu-22.04 | |
| - ubuntu-24.04 | |
| # - ubuntu-latest | |
| # FIXME: the container builds with a recent glibc, use an older | |
| # base system to get a more portable executable. | |
| needs: build | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - uses: cda-tum/setup-z3@main | |
| with: | |
| version: 4.8.5 | |
| - name: Get fstar package | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: ${{ matrix.pak }} | |
| - run: tar xzf ${{ matrix.pak }} | |
| - name: Smoke test | |
| run: | | |
| ./bin/fstar.exe ulib/Prims.fst -f | |
| echo -e "module A\nopen FStar.Mul\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst | |
| ./bin/fstar.exe A.fst | |
| ocaml-smoke: | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| pak: | |
| - fstar-ci-src.tar.gz | |
| - fstar-ci-stage1-src.tar.gz | |
| os: | |
| - ubuntu-20.04 | |
| - ubuntu-22.04 | |
| - ubuntu-24.04 | |
| - ubuntu-latest | |
| exclude: | |
| - os: ubuntu-24.04 # setup-ocaml fails due to darcs https://github.com/ocaml/setup-ocaml/issues/872 | |
| needs: build | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - uses: cda-tum/setup-z3@main | |
| with: | |
| version: 4.8.5 | |
| - name: Get fstar package | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: ${{ matrix.pak }} | |
| - run: tar xzf ${{ matrix.pak }} | |
| - name: Set-up OCaml | |
| uses: ocaml/setup-ocaml@v3 | |
| with: | |
| ocaml-compiler: 4.14.2 | |
| # F* includes an OPAM dependency to Z3, but we are just | |
| # installing a binary with the action above, so we do not | |
| # need it. This is also VERY slow as it builds the binary | |
| # from source. | |
| - run: sed -i '/"z3"/d' fstar.opam | |
| - run: opam install . --deps-only --with-test | |
| - run: eval $(opam env) && make -j$(nproc) | |
| - name: Smoke test | |
| run: | | |
| ./out/bin/fstar.exe out/ulib/Prims.fst -f | |
| echo -e "module A\nopen FStar.Mul\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst | |
| ./out/bin/fstar.exe A.fst | |
| perf-canaries: | |
| needs: build | |
| runs-on: ubuntu-24.04 | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@master | |
| - uses: cda-tum/setup-z3@main | |
| with: | |
| version: 4.8.5 | |
| - name: Get fstar package | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: fstar-ci.tar.gz | |
| - run: tar xzf fstar-ci.tar.gz | |
| - name: Run perf canaries | |
| run: .scripts/perf_canaries.sh ./bin/fstar.exe |