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

Pierre Roux's avatar
Pierre Roux committed
5
.build-common:
6 7
  stage: build
  script:
Pierre Roux's avatar
Pierre Roux committed
8 9 10 11 12 13 14 15 16 17 18 19
    - 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

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

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

Pierre Roux's avatar
Fix CI  
Pierre Roux committed
21
.build-for-process:
22
  stage: build
Pierre Roux's avatar
Fix CI  
Pierre Roux committed
23 24 25 26 27 28 29 30
  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
31 32 33 34 35
  script:
    - ./create_makefile.sh --only-classic
    - make -j ${NJOBS}

.collect-vo-files: 
36 37
  # Keep track of all compiled output and the build infrastructure
  artifacts:
38
    name: prosa-build-files
39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61
    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
62

Pierre Roux's avatar
Pierre Roux committed
63 64 65
1.9.0-coq-8.9:
  extends: .build

66
1.9.0-coq-8.10:
Pierre Roux's avatar
Fix CI  
Pierre Roux committed
67
  extends: .build
68

Pierre Roux's avatar
Pierre Roux committed
69
1.9.0-coq-8.11:
Pierre Roux's avatar
Fix CI  
Pierre Roux committed
70
  extends: .build
Pierre Roux's avatar
Pierre Roux committed
71 72 73 74 75

1.10.0-coq-8.9:
  extends: .build

1.10.0-coq-8.10:
Pierre Roux's avatar
Fix CI  
Pierre Roux committed
76
  extends: .build
Pierre Roux's avatar
Pierre Roux committed
77 78

1.10.0-coq-8.11:
Pierre Roux's avatar
Fix CI  
Pierre Roux committed
79 80 81
  extends: .build

build-for-process:
Pierre Roux's avatar
Pierre Roux committed
82
  extends:
Pierre Roux's avatar
Fix CI  
Pierre Roux committed
83
    - .build-for-process
Pierre Roux's avatar
Pierre Roux committed
84 85
    - .collect-vo-files

Pierre Roux's avatar
Fix CI  
Pierre Roux committed
86
build-for-process-classic:
87
  extends:
Pierre Roux's avatar
Fix CI  
Pierre Roux committed
88
    - .build-for-process-classic
89 90
    - .collect-vo-files

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

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

Pierre Roux's avatar
Pierre Roux committed
103
coq-8.10:
104
  extends:
Pierre Roux's avatar
Pierre Roux committed
105 106
    - .build-dev
  # it's ok to fail with an unreleased version of ssreflect
107
  allow_failure: true
108

Pierre Roux's avatar
Pierre Roux committed
109
coq-dev:
110
  extends:
Pierre Roux's avatar
Pierre Roux committed
111 112
    - .build-dev
  # it's ok to fail with an unreleased version of ssreflect and Coq
113 114
  allow_failure: true

115
validate:
116
  stage: process
Pierre Roux's avatar
Fix CI  
Pierre Roux committed
117 118 119 120 121
  image: mathcomp/mathcomp:1.10.0-coq-8.11
  needs: ["build-for-process"]
  dependencies:
    - build-for-process
  script: make validate
122

123
validate-classic:
124
  stage: process
Pierre Roux's avatar
Fix CI  
Pierre Roux committed
125 126
  image: mathcomp/mathcomp:1.10.0-coq-8.11
  needs: ["build-for-process-classic"]
127
  dependencies:
Pierre Roux's avatar
Fix CI  
Pierre Roux committed
128
    - build-for-process-classic
129 130 131 132
  script: make validate

.doc: 
  stage: process
Pierre Roux's avatar
Fix CI  
Pierre Roux committed
133
  image: mathcomp/mathcomp:1.10.0-coq-8.11
134
  script:
135
    - make html -j ${NJOBS}
136
    - mv html with-proofs
137
    - make gallinahtml -j ${NJOBS}
138
    - mv html without-proofs
139 140
    - make htmlpretty -j ${NJOBS}
    - mv html pretty
141 142 143 144

doc:
  extends:
    - .doc
Pierre Roux's avatar
Fix CI  
Pierre Roux committed
145
  needs: ["build-for-process"]
146
  dependencies:
Pierre Roux's avatar
Fix CI  
Pierre Roux committed
147
    - build-for-process
148 149 150 151 152
  artifacts:
    name: "prosa-spec-$CI_COMMIT_REF_NAME"
    paths:
      - "with-proofs/"
      - "without-proofs/"
153
      - "pretty/"
154
    expire_in: 1 week
155

156 157 158
doc-classic:
  extends:
    - .doc
Pierre Roux's avatar
Fix CI  
Pierre Roux committed
159
  needs: ["build-for-process-classic"]
160
  dependencies:
Pierre Roux's avatar
Fix CI  
Pierre Roux committed
161
    - build-for-process-classic
162 163 164 165 166 167 168 169
  artifacts:
    name: "prosa-classic-spec-$CI_COMMIT_REF_NAME"
    paths:
      - "with-proofs/"
      - "without-proofs/"
      - "pretty/"
    expire_in: 1 week

170 171
proof-state:
  stage: process
Pierre Roux's avatar
Fix CI  
Pierre Roux committed
172 173
  image: mathcomp/mathcomp:1.10.0-coq-8.11
  needs: ["build-for-process"]
174
  dependencies:
Pierre Roux's avatar
Fix CI  
Pierre Roux committed
175
    - build-for-process
176
  script:
Björn Brandenburg's avatar
Björn Brandenburg committed
177
    - find . -iname *.v ! -path './classic/*' | xargs -P ${NJOBS} -n 1 scripts/record-proof-state.py -c '-R . prosa -w -notation-overriden,-parsing' --timeout 20
178
    - scripts/intersperse-proof-state.py `find . -iname *.v ! -path './classic/*'`
179 180 181 182
    - cd with-proof-state/
    - ln -s ../scripts/
    - ln -s ../_CoqProject
    - ../create_makefile.sh
183
    - make -j ${NJOBS}
184 185 186 187 188 189 190
    - 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