.gitlab-ci.yml

stages:
  - build
  - process

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

1.8.0-coq-8.8:
  extends: .build

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

1.9.0-coq-8.9:
  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
   
validate:
  stage: process
  image: mathcomp/mathcomp:1.9.0-coq-8.9
  dependencies:
    - 1.9.0-coq-8.9
  script: make validate

doc:
  stage: process
  image: mathcomp/mathcomp:1.9.0-coq-8.9
  dependencies:
    - 1.9.0-coq-8.9
  script:
    - make html
    - mv html with-proofs
    - make gallinahtml
    - mv html without-proofs
  artifacts:
    name: "prosa-spec-$CI_COMMIT_REF_NAME"
    paths:
      - "with-proofs/"