.gitlab-ci.yml 1.48 KB
Newer Older
1 2 3 4
stages:
  - build
  - process

5 6
.build:
  stage: build
7
  image: mathcomp/mathcomp:${CI_JOB_NAME}
8 9 10 11
  script:
    - ./create_makefile.sh
    - make -j ${NJOBS}

12
1.8.0-coq-8.8:
13 14
  extends: .build

15 16
1.9.0-coq-dev:
  extends: .build
17 18
  # it's ok to fail with an unreleased version of Coq
  allow_failure: true 
19 20 21 22 23

1.9.0-coq-8.9:
  extends: .build
  # Keep track of all compiled output and the build infrastructure
  artifacts:
24
    name: prosa-build-files
25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50
    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:
51
  stage: process
52 53 54 55
  image: mathcomp/mathcomp:1.9.0-coq-8.9
  dependencies:
    - 1.9.0-coq-8.9
  script: make validate
56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72

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/"
      - "without-proofs/"
    expire_in: 1 week