.gitlab-ci.yml 4.29 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
    - 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

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

Pierre Roux's avatar
Pierre Roux committed
16 17 18 19 20 21 22
.build:
  image: mathcomp/mathcomp:${CI_JOB_NAME}
  extends: .build-common

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

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

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

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

69 70 71 72 73 74
1.11.0-coq-8.11:
  extends: .build

1.11.0-coq-8.12:
  extends: .build

Pierre Roux's avatar
Fix CI  
Pierre Roux committed
75
build-for-process:
Pierre Roux's avatar
Pierre Roux committed
76
  extends:
Pierre Roux's avatar
Fix CI  
Pierre Roux committed
77
    - .build-for-process
Pierre Roux's avatar
Pierre Roux committed
78 79
    - .collect-vo-files

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

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

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

97
coq-8.12:
98
  extends:
Pierre Roux's avatar
Pierre Roux committed
99 100
    - .build-dev
  # it's ok to fail with an unreleased version of ssreflect
101
  allow_failure: true
102

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

109
validate:
110 111
  extends:
    - .preferred-stable-version
112
  stage: process
Pierre Roux's avatar
Fix CI  
Pierre Roux committed
113 114 115 116
  needs: ["build-for-process"]
  dependencies:
    - build-for-process
  script: make validate
117

118
validate-classic:
119 120
  extends:
    - .preferred-stable-version
121
  stage: process
Pierre Roux's avatar
Fix CI  
Pierre Roux committed
122
  needs: ["build-for-process-classic"]
123
  dependencies:
Pierre Roux's avatar
Fix CI  
Pierre Roux committed
124
    - build-for-process-classic
125 126 127
  script: make validate

.doc: 
128 129
  extends:
    - .preferred-stable-version
130
  stage: process
131
  script:
132
    - make html -j ${NJOBS}
133
    - mv html with-proofs
134
    - make gallinahtml -j ${NJOBS}
135
    - mv html without-proofs
136 137
    - make htmlpretty -j ${NJOBS}
    - mv html pretty
138 139 140 141

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

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

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