coq-community
[CI] Update
@erikmd @hoheinzollern @CohenCyril apparently we don't have the Docker images for 2.4.0, did something went wrong during the release process?
@erikmd @hoheinzollern some progress but we still get Error response from daemon: No such image: mathcomp/mathcomp:2.4.0-rocq-9.0 is that expected? did I screw up the image name?
Normally this is mathcomp/mathcomp:2.4.0-rocq-prover-9.0. I'll double-check with the generated README anyway
OK I saw the issue, the PR I had approved too-quickly mentioned 9.00 instead of 9.0, will fix this.
FYI @proux01, you'll need to wait that this issue is closed: https://github.com/math-comp/docker-mathcomp/issues/35 I'll try my best to address it today.
(See also this comment for more details: https://github.com/math-comp/docker-mathcomp/issues/35#issuecomment-2842395976 )
FYI @proux01 I just did a release of docker-keeper (that slightly extends its images.yml interpolation capabilities)
TL;DR: if this pipeline succeeds https://gitlab.inria.fr/math-comp/docker-mathcomp/-/pipelines/1171979,
then you'll have a mathcomp:2.4.0-rocq-prover-9.0 image;
(then we'll see if there are remaining errors to address)
FYI @proux01 :
- Good news,
mathcomp/mathcomp:2.4.0-rocq-prover-9.0andmathcomp/mathcomp:2.4.0-rocq-prover-devwere successfully built and deployed - Unfortunately, the
mathcomp/mathcomp:2.4.0-coq-8.19build failed because of some HB/elpi error: https://gitlab.inria.fr/math-comp/docker-mathcomp/-/jobs/5694374 ; any clue from your side?
* Unfortunately, the `mathcomp/mathcomp:2.4.0-coq-8.19` build failed because of some HB/elpi error: https://gitlab.inria.fr/math-comp/docker-mathcomp/-/jobs/5694374 ; any clue from your side?
Maybe HB 1.9.1 is not compatible with Coq 8.19? In which case we should update the opam package?
Maybe HB 1.9.1 is not compatible with Coq 8.19? we should update the opam package?
Certainly, I was thinking about this kind of issue (as an aside, maintaining the opam-based images takes a bit of time, but one of the upsides is that it allows to spot these kind of dependencies issues early 👍)
BTW comparing the failing build https://gitlab.inria.fr/math-comp/docker-mathcomp/-/jobs/5694374 with this successful other job involving mathcomp 2.3.0: https://gitlab.inria.fr/math-comp/docker-mathcomp/-/jobs/5022887 it appears the versions of elpi (1.19.6) and coq-elpi (2.2.3) were the same, unlike HB (1.7.0 -> 1.9.1) so definitely there's something related to HB's compatibility.
Cc @gares according to the CI of hierarchical-builder, what HB release should we use with coq 8.19, elpi 1.19.6, coq-elpi 2.2.3 ?
Strange, I'm not able to reproduce locally, on my 8.19 switch opam install rocq-hierarchy-builder.1.9.1 works fine:
% opam list
# Packages matching: installed
# Name # Installed # Synopsis
angstrom 0.16.0 Parser combinators built for speed and memory-efficiency
atd 2.15.0 Parser for the ATD data format description language
atdgen 2.15.0 Generates efficient JSON serializers, deserializers and validators
atdgen-runtime 2.15.0 Runtime library for code generated by atdgen
atdts 2.15.0 TypeScript code generation for ATD APIs
base v0.16.3 Full standard library replacement for OCaml
base-bigarray base
base-threads base
base-unix base
bigstringaf 0.9.1 Bigstring intrinsics and fast blits based on memcpy/memmove
biniou 1.2.2 Binary data format designed for speed, safety, ease of use and backward compatibility as protocols evolve
camlp-streams 5.0.1 The Stream and Genlex libraries for use with Camlp4 and Camlp5
cmdliner 1.2.0 Declarative definition of command line interfaces for OCaml
conf-bash 1 Virtual package to install the Bash shell
conf-csdp 1 Virtual package relying on a CSDP binary system installation
conf-g++ 1.0 Virtual package relying on the g++ compiler (for C++)
conf-gmp 4 Virtual package relying on a GMP lib system installation
conf-linux-libc-dev 0 Virtual package relying on the installation of the Linux kernel headers files
coq 8.19.2 pinned to version 8.19.2
coq-bignums 9.0.0+coq8.19 Bignums, the Coq library of arbitrarily large numbers
coq-core 8.19.2 The Coq Proof Assistant -- Core Binaries and Tools
coq-elpi 2.2.3 Elpi extension language for Coq
coq-flocq 4.2.0 A formalization of floating-point arithmetic for the Coq system
coq-paramcoq 1.1.3+coq8.19 Plugin for generating parametricity statements to perform refinement proofs
coq-stdlib 8.19.2 The Coq Proof Assistant -- Standard Library
coqide-server 8.19.2 The Coq Proof Assistant, XML protocol server
cppo 1.6.9 Code preprocessor like cpp for OCaml
csexp 1.5.2 Parsing and printing of S-expressions in Canonical form
dune 3.16.0 Fast, portable, and opinionated build system
dune-build-info 3.16.0 Embed build information inside executable
dune-configurator 3.16.0 Helper library for gathering system configuration
easy-format 1.3.4 High-level and functional interface to the Format module of the OCaml standard library
elpi 1.19.6 ELPI - Embeddable λProlog Interpreter
host-arch-x86_64 1 OCaml on amd64 (64-bit)
host-system-other 1 OCaml on an unidentified system
jane-street-headers v0.16.0 Jane Street C header files
jst-config v0.16.0 Compile-time configuration for Jane Street libraries
logs 0.7.0 Logging infrastructure for OCaml
menhir 20240715 An LR(1) parser generator
menhirCST 20240715 Runtime support library for parsers generated by Menhir
menhirLib 20240715 Runtime support library for parsers generated by Menhir
menhirSdk 20240715 Compile-time library for auxiliary tools related to Menhir
num 1.5 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.14.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.14.1 Official release 4.14.1
ocaml-compiler-libs v0.12.4 OCaml compiler libraries repackaged
ocaml-config 2 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
ocaml-syntax-shims 1.0.0 Backport new syntax to older OCaml versions
ocamlbuild 0.14.3 OCamlbuild is a build system with builtin rules to easily build most OCaml projects
ocamlfind 1.9.6 A library manager for OCaml
ocplib-simplex 0.5 A library implementing a simplex algorithm, in a functional style, for solving systems of linear inequalities and optimizi
osdp 1.1.1 OCaml Interface to SDP solvers
parsexp v0.16.0 S-expression parsing library
ppx_assert v0.16.0 Assert-like extension nodes that raise useful errors on failure
ppx_base v0.16.0 Base set of ppx rewriters
ppx_cold v0.16.0 Expands [@cold] into [@inline never][@specialise never][@local never]
ppx_compare v0.16.0 Generation of comparison functions from types
ppx_derivers 1.2.1 Shared [@@deriving] plugin registry
ppx_deriving 6.0.2 Type-driven code generation for OCaml
ppx_deriving_yojson 3.8.0 JSON codec generator for OCaml
ppx_enumerate v0.16.0 Generate a list containing all values of a finite type
ppx_globalize v0.16.0 A ppx rewriter that generates functions to copy local values to the global heap
ppx_hash v0.16.0 A ppx rewriter that generates hash functions from type expressions and definitions
ppx_here v0.16.0 Expands [%here] into its location
ppx_import 1.11.0 A syntax extension for importing declarations from interface files
ppx_inline_test v0.16.1 Syntax extension for writing in-line tests in ocaml code
ppx_optcomp v0.16.0 Optional compilation for OCaml
ppx_sexp_conv v0.16.0 [@@deriving] plugin to generate S-expression conversion functions
ppxlib 0.32.1 Standard infrastructure for ppx rewriters
re 1.11.0 RE is a regular expression library for OCaml
result 1.5 Compatibility Result module
rocq-hierarchy-builder 1.9.1 High level commands to declare and evolve a hierarchy based on packed classes
seq base Compatibility package for OCaml's standard iterator type starting from 4.07.
sexplib v0.16.0 Library for serializing OCaml values to and from S-expressions
sexplib0 v0.16.0 Library containing the definition of S-expressions and some base converters
stdio v0.16.0 Standard IO library for OCaml
stdlib-shims 0.3.0 Backport some of the new stdlib features to older compiler
stringext 1.6.0 Extra string functions for OCaml
time_now v0.16.0 Reports the current time
topkg 1.0.7 The transitory OCaml software packager
uri 4.4.0 An RFC3986 URI/URL parsing library
yojson 2.1.2 Yojson is an optimized parsing and printing library for the JSON format
zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers
@erikmd that being said, the Docker CI of HB seems completely broken: https://github.com/math-comp/hierarchy-builder/actions/runs/14796943582/job/41546267124
Install dependencies
[...]
=== remove 2 packages
- remove coq 8.19.2 (pinned) [conflicts with coq-core]
[...]
=== upgrade 4 packages
[...]
- upgrade coq-core 8.19.2 to 9.0.0 [uses rocq-runtime]
Maybe the images should pin coq-core/rocq-runtime rather than coq?
Thanks for the feedback, BTW it'd be good to understand why, using almost the same versions (in your local switch and in the docker-mathcomp job), HB 1.9.1 fails to build from source saying File "./HB/structures.v", line 17, characters 0-30: Error: Cannot find a physical path bound to logical path elpi with prefix elpi.
using almost the same versions (in your local switch and in the docker-mathcomp job)
Which difference did you spot? The versions of elpi and coq-elpi seem to be the same
Sorry for my vague wording: yes there are no differences, so I'm puzzled that Coq did not find the elpi namespace at that point.
Meanwhile, despite the full-blown renaming, docker-coq only pins the coq package, and docker-rocq only pins the rocq-stdlib, rocq-prover, coqide-server, and I had put the following comment in the Dockerfile:
# We need not pin rocq-core nor rocq-runtime
# as rocq-prover => "rocq-core" {= version}
# and rocq-core => "rocq-runtime" {= version}
but maybe it'd be safer to also pin these core dependencies!
So meanwhile, even if I don't have an immediate answer to the question I asked in my previous comment, I propose to: also pin the core packages in docker-coq/docker-rocq and rebuild them.
Apparently yes, they need to be pinned. I guess the issue didn't manifest until recently due to the coq-core package being virtually useless and everybody actually depending on coq?
yes, this pinning is certainly necessary! as https://github.com/LPCIC/coq-elpi/blob/master/coq-elpi.opam doesn't depend on coq, but on coq-core… so if only coq is pinned (not coq-core), bad things happen! :x: ; Thanks again, Pierre!
Hi @proux01, I believe all the required building blocks for supporting Coq+Rocq with mathcomp stable and dev are now OK. → I launched the build in docker-base at https://github.com/rocq-community/docker-base/commit/caa184b7d75dc27374bfc11ed82547d960127e54 which will, in turn, propagate to docker-coq & docker-rocq, which will, in turn, propagate to (docker)mathcomp & …-dev. If there's some remaining issue (hopefully not), I'll try to address this tomorrow. Stay tuned!
And, thanks for your patience - it took a bit of time just because, as we may have expected, the prover's renaming have had a non-trivial impact on the whole infrastructure.
Hi @erikmd @proux01, is there any news on the mathcomp/mathcomp:2.4.0-coq-8.19 image? It's not there yet.
@pi8027 Nope, I'm really sorry for the delay… this is something I definitely want to look at and fix!
it just happens it's the end of the teaching semester, and I've been swamped with exams' grading :-|
so I'll try to look at this closely this week (ideally on Thursday)… stay tuned 👍
@erikmd Don't worry. I was just wondering whether I should remove it from a CI config for the moment, and it's not a critical issue for me. Thanks a lot for your work in any case!