diff --git a/.github/workflows/build-schools.yml b/.github/workflows/build-schools.yml index 79c0c34..f04b24d 100644 --- a/.github/workflows/build-schools.yml +++ b/.github/workflows/build-schools.yml @@ -1,68 +1,84 @@ -# This is a basic workflow to help you get started with Actions - name: CI # Controls when the action will run. on: - # Triggers the workflow on push or pull request events but only for the master branch + # Run the workflow on push or pull request events but only for the master branch push: branches: [ master ] pull_request: branches: [ master ] + # Run at 05:37 UTC every Thursday to keep the cache from being evicted. schedule: - # Run this workflow at 02:15 UTC every Tuesday to keep the cache from being - # evicted. A typical run with everything cached should take less than 10 - # minutes. - - cron: 15 2 * * TUE + - cron: 37 5 * * THU - # Allows you to run this workflow manually from the Actions tab + # Run when activated manually from the Actions tab workflow_dispatch: -env: - # Set this to the version of Coq that should be used. - coq-version: 8.19.0 - dune-version: 3.8.0 - DUNE_CACHE_STORAGE_MODE: copy - -# A workflow run is made up of one or more jobs that can run sequentially or in parallel jobs: - # This workflow contains a single job called "build" build: - name: Build Schools - # The type of runner that the job will run on - runs-on: ubuntu-latest + strategy: + fail-fast: false + matrix: + os: [ ubuntu-latest ] + coq-version: [ latest ] + ocaml-version: [ default ] - # Steps represent a sequence of tasks that will be executed as part of the job + name: Build Schools on Linux (Coq ${{ matrix.coq-version }}) + runs-on: ${{ matrix.os }} steps: - # Checkout UniMath into the working directory - name: Checkout UniMath. - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: repository: UniMath/UniMath clean: false path: . - # Checkout the current branch into Schools/ - name: Checkout Schools. - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: path: Schools - # Ideally we would use docker-coq. A setup currently takes about 7min - # before it starts compiling, with OCaml cached. - - name: Install OCaml. - uses: ocaml/setup-ocaml@v2 + # The path variable here matches the DUNE_CACHE_ROOT variable in the "Build Schools" step + - name: Load cache + uses: actions/cache/restore@v4 + id: cache + with: + path: dune-cache + key: UniMath-Schools-${{ runner.os }}-coq-${{ matrix.coq-version }}-${{ github.run_id }}-${{ github.run_number }} + restore-keys: | + UniMath-Schools-${{ runner.os }}-coq-${{ matrix.coq-version }}-${{ github.run_id }} + UniMath-Schools-${{ runner.os }}-coq-${{ matrix.coq-version }}- + + - name: Build Schools + uses: coq-community/docker-coq-action@v1 with: - ocaml-compiler: ocaml-variants.4.14.0+options,ocaml-option-flambda - dune-cache: true - opam-disable-sandboxing: true + coq_version: ${{ matrix.coq-version }} + ocaml_version: ${{ matrix.ocaml-version }} + custom_script: | + startGroup "Workaround permission issue" + sudo chown -R coq:coq . + endGroup - - name: Install Dune - run: opam pin add dune ${{ env.dune-version }} - - name: Install Coq - run: opam pin add coq ${{ env.coq-version }} + startGroup "Print versions" + opam --version + opam exec -- dune --version + opam exec -- coqc --version + endGroup - # Schools is built using the flags specified in code/dune. - - name: Compile Schools. - run: opam exec -- dune build Schools --display=short --error-reporting=twice + startGroup "Build UniMath" + export DUNE_CACHE_ROOT=$(pwd)/dune-cache/ + opam exec -- dune build Schools -j 2 --display=short --cache=enabled --error-reporting=twice + endGroup + + # In a separate step, to make sure it runs, even if the previous step fails + - name: Revert permissions + if: ${{ always() }} + run: sudo chown -R 1001:116 . + + - name: Save cache + uses: actions/cache/save@v4 + if: ${{ always() }} + with: + path: dune-cache + key: UniMath-Schools-${{ runner.os }}-coq-${{ matrix.coq-version }}-${{ github.run_id }}-${{ github.run_number }}