.gitlab-ci.yml

stages:
  - build
  - process

.build:
  stage: build
  image: mathcomp/mathcomp:${CI_JOB_NAME}
  script:
    - ./create_makefile.sh
    - make -j ${NJOBS}

1.9.0-coq-8.10:
  extends: .build
  # Keep track of all compiled output and the build infrastructure
  artifacts:
    name: prosa-build-files
    paths:
    - _CoqProject
    - Makefile
    - Makefile.conf
    # Ugly hack around https://gitlab.com/gitlab-org/gitlab-runner/issues/2620
    - "*/*.vo"
    - "*/*/*.vo"
    - "*/*/*/*.vo"
    - "*/*/*/*/*.vo"
    - "*/*/*/*/*/*.vo"
    - "*/*/*/*/*/*/*.vo"
    - "*/*/*/*/*/*/*/*.vo"
    - "*/*/*/*/*/*/*/*/*.vo"
    - "*/*/*/*/*/*/*/*/*/*.vo"
    - "*/*.glob"
    - "*/*/*.glob"
    - "*/*/*/*.glob"
    - "*/*/*/*/*.glob"
    - "*/*/*/*/*/*.glob"
    - "*/*/*/*/*/*/*.glob"
    - "*/*/*/*/*/*/*/*.glob"
    - "*/*/*/*/*/*/*/*/*.glob"
    - "*/*/*/*/*/*/*/*/*/*.glob"
    expire_in: 1 week

proof-length:
  stage: build
  image: python:3-alpine
  script:
    - scripts/proofloc.py --check --long-proofs scripts/known-long-proofs.json `find . -iname *.v`

1.9.0-coq-8.9:
  extends: .build

1.9.0-coq-dev:
  extends: .build
  # it's ok to fail with an unreleased version of Coq
  allow_failure: true

latest-coq-8.10:
  extends: .build
  # it's ok to fail with an unreleased version of ssreflect
  allow_failure: true

validate:
  stage: process
  image: mathcomp/mathcomp:1.9.0-coq-8.10
  needs: ["1.9.0-coq-8.10"]
  dependencies:
    - 1.9.0-coq-8.10
  script: make validate

doc:
  stage: process