stages:
  - build
  - process

.build-common:
  stage: build
  script:
    - opam update -y
    - opam remove -y coq-mathcomp-algebra coq-mathcomp-character coq-mathcomp-field coq-mathcomp-fingroup coq-mathcomp-solvable  # Check coq-mathcomp-ssreflect is enough
    - opam pin add -n -y -k path coq-prosa .
    - opam install -y -v -j ${NJOBS} coq-prosa

.preferred-stable-version:
    image: mathcomp/mathcomp:1.10.0-coq-8.11

.build:
  image: mathcomp/mathcomp:${CI_JOB_NAME}
  extends: .build-common

.build-dev:
  image: mathcomp/mathcomp-dev:${CI_JOB_NAME}
  extends: .build-common

.build-for-process:
  stage: build
  image: mathcomp/mathcomp:1.10.0-coq-8.11
  script:
    - ./create_makefile.sh --without-classic
    - make -j ${NJOBS}

.build-for-process-classic:
  stage: build
  image: mathcomp/mathcomp:1.10.0-coq-8.11
  script:
    - ./create_makefile.sh --only-classic
    - make -j ${NJOBS}

.collect-vo-files: 
  # Keep track of all compiled output and the build infrastructure
  artifacts:
    name: prosa-build-files
    paths:
    - 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

1.10.0-coq-8.11:
  extends: .build

1.11.0-coq-8.11:
  extends: .build

1.11.0-coq-8.12:
  extends: .build

build-for-process:
  extends:
    - .build-for-process
    - .collect-vo-files

build-for-process-classic:
  extends:
    - .build-for-process-classic
    - .collect-vo-files

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

spell-check:
  stage: build
  image: bbbrandenburg/aspell-ci
  script:
    - scripts/flag-typos-in-comments.sh `find .  -iname '*.v' ! -path './classic/*'`

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

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

validate:
  extends:
    - .preferred-stable-version
  stage: process
  needs: ["build-for-process"]
  dependencies:
    - build-for-process
  script: make validate

validate-classic:
  extends:
    - .preferred-stable-version
  stage: process
  needs: ["build-for-process-classic"]
  dependencies:
    - build-for-process-classic
  script: make validate

.doc: 
  extends:
    - .preferred-stable-version
  stage: process
  script:
    - make html -j ${NJOBS}
    - mv html with-proofs
    - make gallinahtml -j ${NJOBS}
    - mv html without-proofs
    - make htmlpretty -j ${NJOBS}
    - mv html pretty

doc:
  extends:
    - .doc
  needs: ["build-for-process"]
  dependencies:
    - build-for-process
  artifacts:
    name: "prosa-spec-$CI_COMMIT_REF_NAME"
    paths:
      - "with-proofs/"
      - "without-proofs/"
      - "pretty/"
    expire_in: 1 week

doc-classic:
  extends:
    - .doc
  needs: ["build-for-process-classic"]
  dependencies:
    - build-for-process-classic
  artifacts:
    name: "prosa-classic-spec-$CI_COMMIT_REF_NAME"
    paths:
      - "with-proofs/"
      - "without-proofs/"
      - "pretty/"
    expire_in: 1 week

proof-state:
  extends:
    - .preferred-stable-version
  stage: process
  needs: ["build-for-process"]
  dependencies:
    - build-for-process
  script:
    - find . -iname *.v ! -path './classic/*' | xargs -P ${NJOBS} -n 1 scripts/record-proof-state.py -c '-R . prosa -w -notation-overriden,-parsing' --timeout 20
    - scripts/intersperse-proof-state.py `find . -iname *.v ! -path './classic/*'`
    - cd with-proof-state/
    - ln -s ../scripts/
    - ln -s ../_CoqProject
    - ../create_makefile.sh
    - make -j ${NJOBS}
    - make html -j ${NJOBS} COQDOCEXTRAFLAGS=--plain-comments
    - mv html ../with-proofs-and-proof-state
  artifacts:
    name: "prosa-proof-state-$CI_COMMIT_REF_NAME"
    paths:
      - "with-proofs-and-proof-state/"
    expire_in: 1 week