Nightly CI #49
This file contains hidden or 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: Nightly CI | |
| # Run the heavier CI checks (opam, nix, smoke tests) on a nightly | |
| # schedule instead of on every push. See ci.yml for context. | |
| on: | |
| schedule: | |
| - cron: '0 2 * * *' | |
| workflow_dispatch: | |
| jobs: | |
| opam: | |
| name: opam | |
| uses: ./.github/workflows/build-opam.yml | |
| nix-build: | |
| name: nix | |
| uses: ./.github/workflows/nix.yml | |
| build: | |
| name: build | |
| uses: ./.github/workflows/build-packages.yml | |
| binary-smoke: | |
| needs: build | |
| runs-on: ubuntu-24.04 | |
| steps: | |
| - name: Get fstar package | |
| uses: actions/download-artifact@v8 | |
| with: | |
| name: fstar.tar.gz | |
| - run: tar xzf fstar.tar.gz | |
| - name: Install Z3 | |
| # Note: the packages built by build-packages.yml don't include Z3. | |
| run: curl -fsSL https://raw.githubusercontent.com/FStarLang/FStar/refs/heads/master/.scripts/get_fstar_z3.sh | sudo bash -s -- /usr/local/bin | |
| - name: Smoke test | |
| run: | | |
| ./fstar/bin/fstar.exe fstar/lib/fstar/ulib/Prims.fst -f | |
| echo -e "module A\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst | |
| ./fstar/bin/fstar.exe A.fst | |
| echo -e "module B\n#lang-pulse\nopen Pulse\nfn test (x:int) returns int { (x+1); }" > B.fst | |
| ./fstar/bin/fstar.exe B.fst | |
| ocaml-smoke: | |
| needs: build | |
| strategy: | |
| matrix: | |
| pak: | |
| - fstar-src.tar.gz | |
| os: | |
| - ubuntu-24.04 | |
| - ubuntu-latest | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - name: Get fstar package | |
| uses: actions/download-artifact@v8 | |
| with: | |
| name: ${{ matrix.pak }} | |
| - run: tar xzf ${{ matrix.pak }} | |
| - name: Install Z3 | |
| run: sudo ./fstar/get_fstar_z3.sh /usr/local/bin | |
| - name: Set-up OCaml | |
| uses: ocaml/setup-ocaml@v3 | |
| with: | |
| ocaml-compiler: 5.3.0 | |
| - run: opam install . --deps-only --with-test | |
| working-directory: fstar | |
| - run: eval $(opam env) && make -kj$(nproc) ADMIT=1 | |
| working-directory: fstar | |
| - name: Smoke test | |
| run: | | |
| ./out/bin/fstar.exe out/lib/fstar/ulib/Prims.fst -f | |
| echo -e "module A\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst | |
| ./out/bin/fstar.exe A.fst | |
| echo -e "module B\n#lang-pulse\nopen Pulse\nfn test (x:int) returns int { (x+1); }" > B.fst | |
| ./out/bin/fstar.exe B.fst | |
| working-directory: fstar |