Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improve the build script, re-enable Search commands #53

Merged
merged 3 commits into from
Aug 30, 2024
Merged
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Next Next commit
Create a new build script, based on the UniMath one
  • Loading branch information
arnoudvanderleer committed Aug 28, 2024
commit 322986e82d2c860abd00bc1fa2793eeb4a01064d
92 changes: 54 additions & 38 deletions .github/workflows/build-schools.yml
Original file line number Diff line number Diff line change
@@ -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 }}
Loading