Skip to content

Commit f9f3beb

Browse files
erikmderikmd
authored
Merge pull request #11 from coq-community/rocq-9.0.0
Release rocq/rocq-prover:9.0.0
2 parents f271edd + 72731c2 commit f9f3beb

File tree

4 files changed

+99
-51
lines changed

4 files changed

+99
-51
lines changed

‎images.yml‎

Lines changed: 53 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ active: true
44
docker_repo: 'rocq/rocq-prover'
55
vars:
66
# TODO: Update when appropriate
7-
rocq_latest: '8.20.1'
7+
rocq_latest: '9.0.0'
88
args:
99
BUILD_DATE: '{defaults[build_date]}'
1010
# propagate:
@@ -101,55 +101,67 @@ images:
101101
- tag: '{matrix[rocq]}-native-flambda'
102102
if: '{matrix[base]} != {matrix[default]}'
103103
################################################################
104-
## rocq/rocq-prover:9.0-rc1
104+
## rocq/rocq-prover:9.0.0
105+
## rocq/rocq-prover:latest
105106
- matrix:
106107
default: ['4.14.2-flambda']
107108
# only *-flambda switches
108109
base: ['4.14.2-flambda', '4.13.1-flambda', '4.12.1-flambda', '4.09.1-flambda']
109-
rocq: ['9.0-rc1']
110-
build: &build_rocq_alpha
110+
rocq: ['9.0.0']
111+
build: &build_rocq_stable
111112
context: './rocq'
112-
dockerfile: './beta/Dockerfile'
113+
dockerfile: './stable/Dockerfile'
113114
keywords:
114-
- '{matrix[rocq][%-*]}'
115+
- '{matrix[rocq][%.*]}'
115116
args:
116117
BASE_TAG: 'rocq_{matrix[base]}'
117-
ROCQ_VERSION: '{matrix[rocq][//-/+]}'
118-
VCS_REF: 'V{matrix[rocq][//-/+]}'
118+
ROCQ_VERSION: '{matrix[rocq]}'
119+
VCS_REF: 'V{matrix[rocq]}'
119120
ROCQ_EXTRA_OPAM: 'rocq-bignums'
120121
# +- rocq-native
121122
tags:
122123
# full tag
123124
- tag: '{matrix[rocq]}-ocaml-{matrix[base]}'
124125
# abbreviated tag (*-ocaml-4.14-flambda)
125-
- tag: '{matrix[rocq][%-*]}-ocaml-{matrix[base][%.*-*]}-flambda'
126-
# default tag (9.0-alpha)
126+
- tag: '{matrix[rocq][%.*]}-ocaml-{matrix[base][%.*-*]}-flambda'
127+
# default tag (9.0.0)
127128
- tag: '{matrix[rocq]}'
128129
if: '{matrix[base]} == {matrix[default]}'
129130
# abbreviated tag (9.0)
130-
- tag: '{matrix[rocq][%-*]}'
131+
- tag: '{matrix[rocq][%.*]}'
131132
if: '{matrix[base]} == {matrix[default]}'
132-
# rocq/rocq-prover:9.0-rc1-native
133+
# latest-abbreviated tag (*-ocaml-4.14-flambda)
134+
- tag: 'latest-ocaml-{matrix[base][%.*-*]}-flambda'
135+
if:
136+
- '{matrix[rocq]} == {vars[rocq_latest]}'
137+
# latest tag
138+
- tag: 'latest'
139+
if:
140+
- '{matrix[rocq]} == {vars[rocq_latest]}'
141+
- '{matrix[base]} == {matrix[default]}'
142+
## rocq/rocq-prover:9.0.0-native
143+
## rocq/rocq-prover:latest-native-flambda
144+
## rocq/rocq-prover:latest-native
133145
- matrix:
134146
default: ['4.14.2']
135147
base: ['4.14.2', '4.14.2-flambda']
136-
rocq: ['9.0-rc1']
137-
build:
138-
<<: *build_rocq_alpha
148+
rocq: ['9.0.0']
149+
build: &build_rocq_stable_native
150+
<<: *build_rocq_stable
139151
args:
140152
BASE_TAG: 'rocq_{matrix[base]}'
141-
ROCQ_VERSION: '{matrix[rocq][//-/+]}'
142-
VCS_REF: 'V{matrix[rocq][//-/+]}'
143-
ROCQ_EXTRA_OPAM: 'rocq-native rocq-bignums'
153+
ROCQ_VERSION: '{matrix[rocq]}'
154+
VCS_REF: 'V{matrix[rocq]}'
155+
ROCQ_EXTRA_OPAM: 'rocq-native coq-native rocq-bignums'
144156
# +- rocq-native
145157
tags:
146158
# full tag
147159
- tag: '{matrix[rocq]}-native-ocaml-{matrix[base]}'
148160
# abbreviated tag (*-ocaml-4.14)
149-
- tag: '{matrix[rocq][%-*]}-native-ocaml-{matrix[base][%.*]}'
161+
- tag: '{matrix[rocq][%.*]}-native-ocaml-{matrix[base][%.*]}'
150162
if: '{matrix[base]} == {matrix[default]}'
151163
# abbreviated tag (*-ocaml-4.14-flambda)
152-
- tag: '{matrix[rocq][%-*]}-native-ocaml-{matrix[base][%.*-*]}-flambda'
164+
- tag: '{matrix[rocq][%.*]}-native-ocaml-{matrix[base][%.*-*]}-flambda'
153165
if: '{matrix[base]} != {matrix[default]}' # -flambda
154166
# default tag (9.0-alpha-native)
155167
- tag: '{matrix[rocq]}-native'
@@ -158,11 +170,30 @@ images:
158170
- tag: '{matrix[rocq]}-native-flambda'
159171
if: '{matrix[base]} != {matrix[default]}' # -flambda
160172
# abbreviated tag (9.0-native)
161-
- tag: '{matrix[rocq][%-*]}-native'
173+
- tag: '{matrix[rocq][%.*]}-native'
162174
if: '{matrix[base]} == {matrix[default]}'
163175
# abbreviated tag (9.0-native-flambda)
164-
- tag: '{matrix[rocq][%-*]}-native-flambda'
176+
- tag: '{matrix[rocq][%.*]}-native-flambda'
165177
if: '{matrix[base]} != {matrix[default]}' # -flambda
178+
# latest-abbreviated tag (latest-native-ocaml-4.13)
179+
- tag: 'latest-native-ocaml-{matrix[base][%.*]}'
180+
if:
181+
- '{matrix[rocq]} == {vars[rocq_latest]}'
182+
- '{matrix[base]} == {matrix[default]}'
183+
# latest-abbreviated tag (latest-native-ocaml-4.13-flambda)
184+
- tag: 'latest-native-ocaml-{matrix[base][%.*]}-flambda'
185+
if:
186+
- '{matrix[rocq]} == {vars[rocq_latest]}'
187+
- '{matrix[base]} != {matrix[default]}' # -flambda
188+
# latest tag
189+
- tag: 'latest-native'
190+
if:
191+
- '{matrix[rocq]} == {vars[rocq_latest]}'
192+
- '{matrix[base]} == {matrix[default]}'
193+
- tag: 'latest-native-flambda'
194+
if:
195+
- '{matrix[rocq]} == {vars[rocq_latest]}'
196+
- '{matrix[base]} != {matrix[default]}' # -flambda
166197
################################################################
167198
# TODO: Uncomment when the v8.21 branch is created
168199
## coqorg/coq:8.21-alpha

‎rocq/beta/Dockerfile‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,12 @@ RUN set -x \
1818
&& opam update -y -u \
1919
&& opam pin add -n -k version rocq-stdlib ${ROCQ_VERSION} \
2020
&& opam pin add -n -k version rocq-prover ${ROCQ_VERSION} \
21-
&& opam install -y -v -j "${NJOBS}" rocq-prover ${ROCQ_EXTRA_OPAM} \
21+
# WE NEED NOT pin rocq-core nor rocq-runtime
22+
# as rocq-prover => "rocq-core" {= version}
23+
# and rocq-core => "rocq-runtime" {= version}
24+
&& opam pin add -n -k version coqide-server ${ROCQ_VERSION} \
25+
# WE DON'T install coq-core nor coq as they're transitional pkgs whose install time is negligible
26+
&& opam install -y -v -j "${NJOBS}" rocq-prover coqide-server ${ROCQ_EXTRA_OPAM} \
2227
&& opam clean -a -c -s --logs \
2328
&& chmod -R g=u /home/rocq/.opam \
2429
&& opam config list && opam list

‎rocq/stable/Dockerfile‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
ARG BASE_TAG="latest"
2+
FROM rocq/base:${BASE_TAG}
3+
4+
ARG ROCQ_EXTRA_OPAM="rocq-bignums"
5+
ENV ROCQ_EXTRA_OPAM="${ROCQ_EXTRA_OPAM}"
6+
7+
ARG ROCQ_VERSION="dev"
8+
ENV ROCQ_VERSION=${ROCQ_VERSION}
9+
10+
# This line is actually unneeded (was already enabled in rocq/base)
11+
SHELL ["/bin/bash", "--login", "-o", "pipefail", "-c"]
12+
13+
# hadolint ignore=SC2046
14+
RUN set -x \
15+
&& eval $(opam env "--switch=${COMPILER}" --set-switch) \
16+
&& opam update -y -u \
17+
&& opam pin add -n -k version rocq-stdlib ${ROCQ_VERSION} \
18+
&& opam pin add -n -k version rocq-prover ${ROCQ_VERSION} \
19+
# WE NEED NOT pin rocq-core nor rocq-runtime
20+
# as rocq-prover => "rocq-core" {= version}
21+
# and rocq-core => "rocq-runtime" {= version}
22+
&& opam pin add -n -k version coqide-server ${ROCQ_VERSION} \
23+
# WE DON'T install coq-core nor coq as they're transitional pkgs whose install time is negligible
24+
&& opam install -y -v -j "${NJOBS}" rocq-prover coqide-server ${ROCQ_EXTRA_OPAM} \
25+
&& opam clean -a -c -s --logs \
26+
&& chmod -R g=u /home/rocq/.opam \
27+
&& opam config list && opam list
28+
29+
ARG BUILD_DATE
30+
ARG VCS_REF
31+
LABEL org.label-schema.build-date=${BUILD_DATE} \
32+
org.label-schema.name="The Rocq Prover" \
33+
org.label-schema.description="Rocq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs." \
34+
org.label-schema.url="https://rocq-prover.org/" \
35+
org.label-schema.vcs-ref=${VCS_REF} \
36+
org.label-schema.vcs-url="https://github.com/coq/coq" \
37+
org.label-schema.vendor="The Rocq Development Team" \
38+
org.label-schema.version=${ROCQ_VERSION} \
39+
org.label-schema.schema-version="1.0" \
40+
maintainer="erik@martin-dorel.org"

‎stable/Dockerfile‎

Lines changed: 0 additions & 28 deletions
This file was deleted.

0 commit comments

Comments
 (0)