File tree Expand file tree Collapse file tree 4 files changed +44
-0
lines changed Expand file tree Collapse file tree 4 files changed +44
-0
lines changed Original file line number Diff line number Diff line change 87
87
- NJOBS =2
88
88
<<: *OPAM
89
89
{ { / tested_coq_opam_versions } }
90
+ # Test supported versions of Rocq via OPAM
91
+ { { # tested_rocq_opam_versions } }
92
+ - env:
93
+ - COQ_IMAGE ={ { repo } } { { ^ repo } } rocq /rocq-prover{{ / repo }}:{{ version }}
94
+ - PACKAGE ={ { opam_name } } { { ^ opam_name } } coq-{{ shortname }}{{ / opam_name }}.{{ opam-file-version }}{{^ opam-file-version }}dev{{ / opam-file-version }}
95
+ - NJOBS =2
96
+ <<: *OPAM
97
+ { { / tested_rocq_opam_versions } }
90
98
91
99
{ { # extracted } }
92
100
# Test extracted supported versions of Coq via OPAM
Original file line number Diff line number Diff line change @@ -66,3 +66,8 @@ workflows:
66
66
name: "{ { repo } }{ {^ repo } }Coq{ {/ repo } } { { version } }"
67
67
coq: "{ { repo } }{ {^ repo } }coqorg/coq{ {/ repo } }:{ { version } }"
68
68
{ {/ tested_coq_opam_versions } }
69
+ { {# tested_rocq_opam_versions } }
70
+ - build:
71
+ name: "{ { repo } }{ {^ repo } }Rocq{ {/ repo } } { { version } }"
72
+ coq: "{ { repo } }{ {^ repo } }rocq/rocq-prover{ {/ repo } }:{ { version } }"
73
+ { {/ tested_rocq_opam_versions } }
Original file line number Diff line number Diff line change 24
24
{ {# tested_coq_opam_versions } }
25
25
- '{ { repo } }{ {^ repo } }coqorg/coq{ {/ repo } }:{ { version } }'
26
26
{ {/ tested_coq_opam_versions } }
27
+ { {# tested_rocq_opam_versions } }
28
+ - '{ { repo } }{ {^ repo } }rocq/rocq-prover{ {/ repo } }:{ { version } }'
29
+ { {/ tested_rocq_opam_versions } }
27
30
fail-fast: false
28
31
steps:
29
32
- uses: actions/checkout@v4
Original file line number Diff line number Diff line change @@ -477,6 +477,34 @@ fields:
477
477
- .travis.yml
478
478
- docker-action.yml
479
479
- config.yml
480
+ - tested_rocq_opam_versions :
481
+ type : list
482
+ item_fields :
483
+ - version :
484
+ required : true
485
+ description : >
486
+ Docker tag supported by rocq/rocq-prover:
487
+ https://hub.docker.com/r/rocq/rocq-prover/tags
488
+ Quote the strings, otherwise '9.10' becomes '9.1'.
489
+ examples :
490
+ - " 9.0"
491
+ - " dev-native-flambda"
492
+ - repo :
493
+ required : false
494
+ description : >
495
+ Docker repository supporting the given docker tag.
496
+ Defaults to 'rocq/rocq-prover'.
497
+ examples :
498
+ - " mathcomp/mathcomp"
499
+ - " mathcomp/mathcomp-dev"
500
+ used :
501
+ - .travis.yml
502
+ - docker-action.yml
503
+ - config.yml
504
+ used :
505
+ - .travis.yml
506
+ - docker-action.yml
507
+ - config.yml
480
508
- ci_cron_schedule :
481
509
required : false
482
510
description : >
You can’t perform that action at this time.
0 commit comments