(for PR #29883)
2026-05-08 18:45.20: New job: build lstar-rocq.1.0, using opam dev
from https://github.com/ocaml/opam-repository.git#refs/pull/29883/head (e5ab047b033e89fa4026a3a78b062664a0cf8a36)
on centos-10-ocaml-5.4/amd64
To reproduce locally:
cd $(mktemp -d)
git clone --recursive "https://github.com/ocaml/opam-repository.git" && cd "opam-repository" && git fetch origin "refs/pull/29883/head" && git reset --hard e5ab047b
git fetch origin master
git merge --no-edit fc08333d1ba03c1ffbc960479a92aa94085c5f78
cat > ../Dockerfile <<'END-OF-DOCKERFILE'
FROM ocaml/opam:centos-10-ocaml-5.4@sha256:2ac85e27ea6ff5f9df90a49fee2e39d38529110b605df0299247f2d29a075f85
USER 1000:1000
WORKDIR /home/opam
RUN sudo ln -f /usr/bin/opam-dev /usr/bin/opam
RUN opam init --reinit -ni
RUN opam option solver=builtin-0install && opam config report
ENV OPAMDOWNLOADJOBS="1"
ENV OPAMERRLOGLEN="0"
ENV OPAMPRECISETRACKING="1"
ENV CI="true"
ENV OPAM_REPO_CI="true"
RUN rm -rf opam-repository/
COPY --chown=1000:1000 . opam-repository/
RUN opam repository set-url --strict default opam-repository/
RUN opam update --depexts || true
RUN opam pin add -k version -yn lstar-rocq.1.0 1.0
RUN opam reinstall lstar-rocq.1.0; \
res=$?; \
test "$res" != 31 && exit "$res"; \
export OPAMCLI=2.0; \
build_dir=$(opam var prefix)/.opam-switch/build; \
failed=$(ls "$build_dir"); \
partial_fails=""; \
for pkg in $failed; do \
if opam show -f x-ci-accept-failures: "$pkg" | grep -qF "\"centos-10\""; then \
echo "A package failed and has been disabled for CI using the 'x-ci-accept-failures' field."; \
fi; \
test "$pkg" != 'lstar-rocq.1.0' && partial_fails="$partial_fails $pkg"; \
done; \
test "${partial_fails}" != "" && echo "opam-repo-ci detected dependencies failing: ${partial_fails}"; \
exit 1
END-OF-DOCKERFILE
docker build -f ../Dockerfile .
2026-05-08 18:45.20: Using cache hint "ocaml/opam:centos-10-ocaml-5.4@sha256:2ac85e27ea6ff5f9df90a49fee2e39d38529110b605df0299247f2d29a075f85-lstar-rocq.1.0-e5ab047b033e89fa4026a3a78b062664a0cf8a36"
2026-05-08 18:45.20: Using OBuilder spec:
((from ocaml/opam:centos-10-ocaml-5.4@sha256:2ac85e27ea6ff5f9df90a49fee2e39d38529110b605df0299247f2d29a075f85)
(user (uid 1000) (gid 1000))
(workdir /home/opam)
(run (shell "sudo ln -f /usr/bin/opam-dev /usr/bin/opam"))
(run (network host)
(shell "opam init --reinit --config .opamrc-sandbox -ni"))
(run (shell "opam option solver=builtin-0install && opam config report"))
(env OPAMDOWNLOADJOBS 1)
(env OPAMERRLOGLEN 0)
(env OPAMPRECISETRACKING 1)
(env CI true)
(env OPAM_REPO_CI true)
(run (shell "rm -rf opam-repository/"))
(copy (src .) (dst opam-repository/))
(run (shell "opam repository set-url --strict default opam-repository/"))
(run (network host)
(shell "opam update --depexts || true"))
(run (shell "opam pin add -k version -yn lstar-rocq.1.0 1.0"))
(run (cache (opam-archives (target /home/opam/.opam/download-cache)))
(network host)
(shell "opam reinstall lstar-rocq.1.0;\
\n res=$?;\
\n test \"$res\" != 31 && exit \"$res\";\
\n export OPAMCLI=2.0;\
\n build_dir=$(opam var prefix)/.opam-switch/build;\
\n failed=$(ls \"$build_dir\");\
\n partial_fails=\"\";\
\n for pkg in $failed; do\
\n if opam show -f x-ci-accept-failures: \"$pkg\" | grep -qF \"\\\"centos-10\\\"\"; then\
\n echo \"A package failed and has been disabled for CI using the 'x-ci-accept-failures' field.\";\
\n fi;\
\n test \"$pkg\" != 'lstar-rocq.1.0' && partial_fails=\"$partial_fails $pkg\";\
\n done;\
\n test \"${partial_fails}\" != \"\" && echo \"opam-repo-ci detected dependencies failing: ${partial_fails}\";\
\n exit 1"))
)
2026-05-08 18:45.20: Waiting for resource in pool OCluster
2026-05-08 18:45.20: Waiting for worker…
2026-05-08 18:45.22: Got resource from pool OCluster
Building on eumache.caelum.ci.dev
All commits already cached
HEAD is now at fc08333d1b Merge pull request #29875 from ocaml/mseri-patch-3
Updating fc08333d1b..e5ab047b03
Fast-forward
packages/lstar-rocq/lstar-rocq.1.0/opam | 39 +++++++++++++++++++++++++++++++++
packages/lstar/lstar.1.0/opam | 38 ++++++++++++++++++++++++++++++++
2 files changed, 77 insertions(+)
create mode 100644 packages/lstar-rocq/lstar-rocq.1.0/opam
create mode 100644 packages/lstar/lstar.1.0/opam
(from ocaml/opam:centos-10-ocaml-5.4@sha256:2ac85e27ea6ff5f9df90a49fee2e39d38529110b605df0299247f2d29a075f85)
Unable to find image 'ocaml/opam:centos-10-ocaml-5.4@sha256:2ac85e27ea6ff5f9df90a49fee2e39d38529110b605df0299247f2d29a075f85' locally
docker.io/ocaml/opam@sha256:2ac85e27ea6ff5f9df90a49fee2e39d38529110b605df0299247f2d29a075f85: Pulling from ocaml/opam
4de4001a0d5d: Pulling fs layer
510b52436bdf: Pulling fs layer
5f24283b1d0f: Pulling fs layer
11a888936145: Pulling fs layer
4de4001a0d5d: Waiting
510b52436bdf: Waiting
249550217bb7: Pulling fs layer
5f24283b1d0f: Waiting
a0e21f56eaf7: Pulling fs layer
0b684e941d88: Pulling fs layer
249550217bb7: Waiting
11a888936145: Waiting
a0e21f56eaf7: Waiting
88340d56f57c: Pulling fs layer
0b684e941d88: Waiting
0032ab402594: Pulling fs layer
88340d56f57c: Waiting
30621f9f793f: Pulling fs layer
0032ab402594: Waiting
e3a51685d3be: Pulling fs layer
f80bcdba748f: Pulling fs layer
30621f9f793f: Waiting
376bc233a86e: Pulling fs layer
e3a51685d3be: Waiting
7e570d2973bd: Pulling fs layer
376bc233a86e: Waiting
275ee8ef8196: Pulling fs layer
f80bcdba748f: Waiting
7e570d2973bd: Waiting
dc0f2e51b258: Pulling fs layer
275ee8ef8196: Waiting
79db6360424f: Pulling fs layer
dc0f2e51b258: Waiting
ad69d62ef5fd: Pulling fs layer
ad69d62ef5fd: Waiting
3ff9ff41df93: Pulling fs layer
79db6360424f: Waiting
99b53e1dfa07: Pulling fs layer
3ff9ff41df93: Waiting
80780d5bbe27: Pulling fs layer
99b53e1dfa07: Waiting
b1084ac6755d: Pulling fs layer
80780d5bbe27: Waiting
4f4fb700ef54: Pulling fs layer
b1084ac6755d: Waiting
36e8b7b0ed88: Pulling fs layer
4f4fb700ef54: Waiting
b86c27aac171: Pulling fs layer
36e8b7b0ed88: Waiting
989db563c5e8: Pulling fs layer
e1a4656ab4d2: Pulling fs layer
b86c27aac171: Waiting
a3d45e111a4b: Pulling fs layer
e1a4656ab4d2: Waiting
c61a460f89cf: Pulling fs layer
a3d45e111a4b: Waiting
d630199bb8d9: Pulling fs layer
c61a460f89cf: Waiting
7f1bf2ea605c: Pulling fs layer
cf86a828a23f: Pulling fs layer
d630199bb8d9: Waiting
b728c43dd450: Pulling fs layer
7f1bf2ea605c: Waiting
cf86a828a23f: Waiting
69f1d2456151: Pulling fs layer
8e22281392e7: Pulling fs layer
b728c43dd450: Waiting
0a25f233ab83: Pulling fs layer
69f1d2456151: Waiting
8e22281392e7: Waiting
8db14ab87998: Pulling fs layer
91af2f522975: Pulling fs layer
0a25f233ab83: Waiting
8db14ab87998: Waiting
32aebdc60b85: Pulling fs layer
91af2f522975: Waiting
2bbaf73793a1: Pulling fs layer
d3d6c81122c0: Pulling fs layer
2bbaf73793a1: Waiting
32aebdc60b85: Waiting
d465c073fa1a: Pulling fs layer
9cf77ef369fd: Pulling fs layer
d465c073fa1a: Waiting
1f98273eed3c: Pulling fs layer
d3d6c81122c0: Waiting
e10def39276d: Pulling fs layer
1f98273eed3c: Waiting
9cf77ef369fd: Waiting
916b456341c1: Pulling fs layer
e10def39276d: Waiting
916b456341c1: Waiting
4de4001a0d5d: Verifying Checksum
4de4001a0d5d: Download complete
510b52436bdf: Verifying Checksum
510b52436bdf: Download complete
5f24283b1d0f: Verifying Checksum
5f24283b1d0f: Download complete
11a888936145: Verifying Checksum
11a888936145: Download complete
249550217bb7: Verifying Checksum
249550217bb7: Download complete
a0e21f56eaf7: Download complete
0b684e941d88: Verifying Checksum
0b684e941d88: Download complete
88340d56f57c: Verifying Checksum
88340d56f57c: Download complete
30621f9f793f: Verifying Checksum
30621f9f793f: Download complete
0032ab402594: Verifying Checksum
0032ab402594: Download complete
e3a51685d3be: Verifying Checksum
e3a51685d3be: Download complete
f80bcdba748f: Verifying Checksum
f80bcdba748f: Download complete
376bc233a86e: Verifying Checksum
376bc233a86e: Download complete
dc0f2e51b258: Verifying Checksum
dc0f2e51b258: Download complete
79db6360424f: Verifying Checksum
79db6360424f: Download complete
275ee8ef8196: Verifying Checksum
275ee8ef8196: Download complete
7e570d2973bd: Verifying Checksum
7e570d2973bd: Download complete
4de4001a0d5d: Pull complete
510b52436bdf: Pull complete
ad69d62ef5fd: Verifying Checksum
ad69d62ef5fd: Download complete
3ff9ff41df93: Download complete
99b53e1dfa07: Verifying Checksum
99b53e1dfa07: Download complete
5f24283b1d0f: Pull complete
80780d5bbe27: Download complete
b1084ac6755d: Verifying Checksum
b1084ac6755d: Download complete
4f4fb700ef54: Verifying Checksum
4f4fb700ef54: Download complete
36e8b7b0ed88: Verifying Checksum
36e8b7b0ed88: Download complete
b86c27aac171: Download complete
989db563c5e8: Download complete
e1a4656ab4d2: Verifying Checksum
e1a4656ab4d2: Download complete
a3d45e111a4b: Verifying Checksum
a3d45e111a4b: Download complete
c61a460f89cf: Download complete
d630199bb8d9: Download complete
7f1bf2ea605c: Verifying Checksum
7f1bf2ea605c: Download complete
cf86a828a23f: Verifying Checksum
cf86a828a23f: Download complete
b728c43dd450: Verifying Checksum
b728c43dd450: Download complete
69f1d2456151: Verifying Checksum
69f1d2456151: Download complete
8e22281392e7: Verifying Checksum
8e22281392e7: Download complete
8db14ab87998: Verifying Checksum
8db14ab87998: Download complete
32aebdc60b85: Download complete
2bbaf73793a1: Download complete
d3d6c81122c0: Verifying Checksum
d3d6c81122c0: Download complete
0a25f233ab83: Verifying Checksum
0a25f233ab83: Download complete
d465c073fa1a: Verifying Checksum
d465c073fa1a: Download complete
1f98273eed3c: Verifying Checksum
1f98273eed3c: Download complete
e10def39276d: Download complete
916b456341c1: Verifying Checksum
916b456341c1: Download complete
91af2f522975: Verifying Checksum
91af2f522975: Download complete
9cf77ef369fd: Verifying Checksum
9cf77ef369fd: Download complete
11a888936145: Pull complete
249550217bb7: Pull complete
a0e21f56eaf7: Pull complete
0b684e941d88: Pull complete
88340d56f57c: Pull complete
0032ab402594: Pull complete
30621f9f793f: Pull complete
e3a51685d3be: Pull complete
f80bcdba748f: Pull complete
376bc233a86e: Pull complete
7e570d2973bd: Pull complete
275ee8ef8196: Pull complete
dc0f2e51b258: Pull complete
79db6360424f: Pull complete
ad69d62ef5fd: Pull complete
3ff9ff41df93: Pull complete
99b53e1dfa07: Pull complete
80780d5bbe27: Pull complete
b1084ac6755d: Pull complete
4f4fb700ef54: Pull complete
36e8b7b0ed88: Pull complete
b86c27aac171: Pull complete
989db563c5e8: Pull complete
e1a4656ab4d2: Pull complete
a3d45e111a4b: Pull complete
c61a460f89cf: Pull complete
d630199bb8d9: Pull complete
7f1bf2ea605c: Pull complete
cf86a828a23f: Pull complete
b728c43dd450: Pull complete
69f1d2456151: Pull complete
8e22281392e7: Pull complete
0a25f233ab83: Pull complete
8db14ab87998: Pull complete
91af2f522975: Pull complete
32aebdc60b85: Pull complete
2bbaf73793a1: Pull complete
d3d6c81122c0: Pull complete
d465c073fa1a: Pull complete
9cf77ef369fd: Pull complete
1f98273eed3c: Pull complete
e10def39276d: Pull complete
916b456341c1: Pull complete
Digest: sha256:2ac85e27ea6ff5f9df90a49fee2e39d38529110b605df0299247f2d29a075f85
Status: Downloaded newer image for ocaml/opam@sha256:2ac85e27ea6ff5f9df90a49fee2e39d38529110b605df0299247f2d29a075f85
2026-05-08 18:49.12 ---> saved as "d189f4b281a312bc48a9c3884022c78234a2c3d549a0711c7a88b95d7f3577bf"
/: (user (uid 1000) (gid 1000))
/: (workdir /home/opam)
/home/opam: (run (shell "sudo ln -f /usr/bin/opam-dev /usr/bin/opam"))
2026-05-08 18:49.12 ---> saved as "e7bb7662a8c656133bfd3a697dc7f6118fa0a3eb162486c4926922ec2b5b287b"
/home/opam: (run (network host)
(shell "opam init --reinit --config .opamrc-sandbox -ni"))
Configuring from /home/opam/.opamrc-sandbox, then /home/opam/.opamrc, and finally from built-in defaults.
Checking for available remotes: rsync and local, git.
- you won't be able to use mercurial repositories unless you install the hg command on your system.
- you won't be able to use darcs repositories unless you install the darcs command on your system.
This version of opam requires an update to the layout of /home/opam/.opam from version 2.0 to version 2.2, which can't be reverted.
You may want to back it up before going further.
Continue? [Y/n] y
Format upgrade done.
<><> Updating repositories ><><><><><><><><><><><><><><><><><><><><><><><><><><>
[default] Initialised
2026-05-08 18:49.40 ---> saved as "d523c10e3dbba743f84eacb49f4aaa58f4637344d04a60fcdeb18d437c81583c"
/home/opam: (run (shell "opam option solver=builtin-0install && opam config report"))
Set to 'builtin-0install' the field solver in global configuration
# opam config report
# opam-version 2.5.1
# self-upgrade no
# system arch=x86_64 os=linux os-distribution=centos os-version=10
# solver builtin-0install
# install-criteria -changed,-count[avoid-version,solution]
# upgrade-criteria -count[avoid-version,solution]
# jobs 71
# repositories 1 (version-controlled)
# pinned 1 (version)
# current-switch 5.4
# invariant ["ocaml-base-compiler" {= "5.4.1"}]
# compiler-packages ocaml-base-compiler.5.4.1, ocaml-compiler.5.4.1, ocaml-options-vanilla.1
# ocaml:native true
# ocaml:native-tools true
# ocaml:native-dynlink true
# ocaml:stubsdir /home/opam/.opam/5.4/lib/ocaml/stublibs:/home/opam/.opam/5.4/lib/ocaml
# ocaml:preinstalled false
# ocaml:compiler 5.4.1
2026-05-08 18:49.41 ---> saved as "95c8ee6ba6e5d747d0fa03b4efe0182c58d8f2f08a3e422f6f5f17fe1519db82"
/home/opam: (env OPAMDOWNLOADJOBS 1)
/home/opam: (env OPAMERRLOGLEN 0)
/home/opam: (env OPAMPRECISETRACKING 1)
/home/opam: (env CI true)
/home/opam: (env OPAM_REPO_CI true)
/home/opam: (run (shell "rm -rf opam-repository/"))
2026-05-08 18:49.48 ---> saved as "02cd96105f344f908b8fbff25c28f93cbf05bc66071af96dedfc9c2643674f1d"
/home/opam: (copy (src .) (dst opam-repository/))
2026-05-08 18:49.57 ---> saved as "21b16022f0f6b3906bc2cd43fb1d13e4080d872232ce4c41db9a8da9d5ebb827"
/home/opam: (run (shell "opam repository set-url --strict default opam-repository/"))
[default] Initialised
2026-05-08 18:50.17 ---> saved as "e1c57e78972a68d23a00cb59fa2635d0f57d085527ba6cea4876be6a417b18b0"
/home/opam: (run (network host)
(shell "opam update --depexts || true"))
+ /usr/bin/sudo "yum" "makecache"
- CentOS Stream 10 - BaseOS 74 kB/s | 15 kB 00:00
- CentOS Stream 10 - BaseOS 8.6 MB/s | 6.9 MB 00:00
- CentOS Stream 10 - AppStream 113 kB/s | 15 kB 00:00
- CentOS Stream 10 - AppStream 1.0 MB/s | 3.6 MB 00:03
- CentOS Stream 10 - CRB 114 kB/s | 15 kB 00:00
- CentOS Stream 10 - CRB 1.5 MB/s | 838 kB 00:00
- CentOS Stream 10 - Extras packages 125 kB/s | 16 kB 00:00
- Metadata cache created.
2026-05-08 18:50.28 ---> saved as "30008c62886656f37c95c47eb86242e40b899e51a8ebcbe8a51661ec761af096"
/home/opam: (run (shell "opam pin add -k version -yn lstar-rocq.1.0 1.0"))
lstar-rocq is now pinned to version 1.0
2026-05-08 18:50.29 ---> saved as "0d81809bc9e100d0a3fb5539332b3d00c96f013bfa6fee86f22b78dc1531e651"
/home/opam: (run (cache (opam-archives (target /home/opam/.opam/download-cache)))
(network host)
(shell "opam reinstall lstar-rocq.1.0;\
\n res=$?;\
\n test \"$res\" != 31 && exit \"$res\";\
\n export OPAMCLI=2.0;\
\n build_dir=$(opam var prefix)/.opam-switch/build;\
\n failed=$(ls \"$build_dir\");\
\n partial_fails=\"\";\
\n for pkg in $failed; do\
\n if opam show -f x-ci-accept-failures: \"$pkg\" | grep -qF \"\\\"centos-10\\\"\"; then\
\n echo \"A package failed and has been disabled for CI using the 'x-ci-accept-failures' field.\";\
\n fi;\
\n test \"$pkg\" != 'lstar-rocq.1.0' && partial_fails=\"$partial_fails $pkg\";\
\n done;\
\n test \"${partial_fails}\" != \"\" && echo \"opam-repo-ci detected dependencies failing: ${partial_fails}\";\
\n exit 1"))
lstar-rocq.1.0 is not installed. Install it? [Y/n] y
The following actions will be performed:
=== install 11 packages
- install conf-gmp 5 [required by zarith]
- install conf-linux-libc-dev 0 [required by rocq-runtime]
- install conf-pkg-config 4 [required by zarith]
- install dune 3.23.0 [required by lstar-rocq]
- install lstar-rocq 1.0 (pinned)
- install ocamlfind 1.9.8 [required by rocq-runtime]
- install rocq-core 9.1.1 [required by rocq-prover]
- install rocq-prover meta.1 [required by lstar-rocq]
- install rocq-runtime 9.1.1 [required by rocq-core, rocq-stdlib]
- install rocq-stdlib 9.0.0 [required by rocq-prover]
- install zarith 1.14 [required by rocq-runtime]
The following system packages will first need to be installed:
gmp-devel
<><> Handling external dependencies <><><><><><><><><><><><><><><><><><><><><><>
opam believes some required external dependencies are missing. opam can:
> 1. Run yum to install them (may need root/sudo access)
2. Display the recommended yum command and wait while you run it manually (e.g. in another terminal)
3. Continue anyway, and, upon success, permanently register that this external dependency is present, but not detectable
4. Abort the installation
[1/2/3/4] 1
+ /usr/bin/sudo "yum" "install" "-y" "gmp-devel"
- Last metadata expiration check: 0:00:06 ago on Fri May 8 18:50:27 2026.
- Dependencies resolved.
- ================================================================================
- Package Architecture Version Repository Size
- ================================================================================
- Installing:
- gmp-devel x86_64 1:6.2.1-12.el10 appstream 174 k
- Installing dependencies:
- gmp-c++ x86_64 1:6.2.1-12.el10 appstream 20 k
-
- Transaction Summary
- ================================================================================
- Install 2 Packages
-
- Total download size: 194 k
- Installed size: 382 k
- Downloading Packages:
- (1/2): gmp-c++-6.2.1-12.el10.x86_64.rpm 103 kB/s | 20 kB 00:00
- (2/2): gmp-devel-6.2.1-12.el10.x86_64.rpm 607 kB/s | 174 kB 00:00
- --------------------------------------------------------------------------------
- Total 468 kB/s | 194 kB 00:00
- Running transaction check
- Transaction check succeeded.
- Running transaction test
- Transaction test succeeded.
- Running transaction
- Preparing : 1/1
- Installing : gmp-c++-1:6.2.1-12.el10.x86_64 1/2
- Installing : gmp-devel-1:6.2.1-12.el10.x86_64 2/2
- Running scriptlet: gmp-devel-1:6.2.1-12.el10.x86_64 2/2
-
- Installed:
- gmp-c++-1:6.2.1-12.el10.x86_64 gmp-devel-1:6.2.1-12.el10.x86_64
-
- Complete!
+ /usr/bin/rpm "-q" "--whatprovides" "gmp-devel"
- gmp-devel-6.2.1-12.el10.x86_64
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> retrieved conf-gmp.5 (cached)
-> installed conf-gmp.5
-> installed conf-pkg-config.4
-> installed conf-linux-libc-dev.0
-> retrieved dune.3.23.0 (cached)
-> retrieved lstar-rocq.1.0 (cached)
-> retrieved ocamlfind.1.9.8 (cached)
-> retrieved rocq-core.9.1.1, rocq-runtime.9.1.1 (https://opam.ocaml.org/cache)
-> retrieved rocq-stdlib.9.0.0 (cached)
-> retrieved zarith.1.14 (cached)
-> installed ocamlfind.1.9.8
-> installed zarith.1.14
-> installed dune.3.23.0
-> installed rocq-runtime.9.1.1
-> installed rocq-core.9.1.1
-> installed rocq-stdlib.9.0.0
-> installed rocq-prover.meta.1
-> installed lstar-rocq.1.0
Done.
# To update the current shell environment, run: eval $(opam env)
2026-05-08 18:55.42 ---> saved as "4c270dd44dceb9b290e11169dc3e8c82c0f577698774a6662d7a6502552ee9a0"
Job succeeded
2026-05-08 18:55.49: Job succeeded