[question] New depopt in Coq 8.19.2 and later: memprof-limits

[ejgallego]

Dear Docker Coq developers:

since Coq 8.19.2, Coq contains support for memprof-limits. This is a great feature for those wanting to do real-time checking in Coq, unfortunately the dependency Coq has is optional (encoded using depopt in opam).

This is a problem as the Coq Docker images will rebuild Coq if memprof-limits is installed for example by unrelated packages in CI.

I am not sure what to do here, I see several options:

• introducing a new variant: this could be too heavy? On the other hand I would be happy with a single image let's say with OCaml 4.14.2 and memprof-limits
• installing memprof-limits by default: I think that should work as we plan on making the dependency non-optional in the future. It should not have any impact that we can see, but that's in theory
• do nothing: IMHO we should at least document this issue then

I cc: @SkySkimmer as he's knowledgeable upstream.

[SkySkimmer]

installing memprof-limits by default: I think that should work as we plan on making the dependency non-optional in the future. It should not have any impact that we can see, but that's in theory

I don't know of such a plan but installing memprof-limits by default in the docker images should be fine.

[ejgallego]

I don't know of such a plan but installing memprof-limits by default in the docker images should be fine.

IIRC we only made it depopt because OCaml 5.x still doesn't support memprof-limits

I understood that some point a non-conditional dependency may arrive as IMHO the features of memprof-limits are quite important for Rocq.

@SkySkimmer I think indeed it should be fine too, so I'll propose a patch if the maintainers agree. The footprint of the library is a 100k archive (total footprint on the image depends on how many times the archive is linked to other binaries)

[erikmd]

Hi!
Thanks for opening this.
Reading https://opam.ocaml.org/packages/memprof-limits/, it seems it's very useful for profiling.

Is there any "drawback" for installing the package? (apart from the size - as n×100kB looks fine)
Or in other words, is there a reason for which it wasn't a mandatory dependency?

[erikmd]

Anyway, I'll be happy to add one such useful dependency in the base image of Docker-Coq/Docker-Rocq.

What about adding it by default for coqorg/coq:vX-ocaml-vY for vX ≥ 8.19.2, vY < 5.0 ?

(Actually, all Docker-Coq images are installed with a 4.x ocaml compiler currently; this will evolve soonish to add 5.x as well)

[ejgallego]

@erikmd that sounds good to me thanks!

Let me know if you would like me to submit a PR.

[erikmd]

Let me know if you would like me to submit a PR.

Sure! thanks for proposing your help.

FYI you may want to rely on some build-arg environment variable, maybe just modifying COQ_EXTRA_OPAM:

https://github.com/coq-community/docker-coq/blob/b23763b82383c515e5044325cd7cf31a24565ba7/images.yml#L59

so the Dockerfiles could be kept as is?

https://github.com/coq-community/docker-coq/blob/b23763b82383c515e5044325cd7cf31a24565ba7/coq/stable/Dockerfile#L17-L24

or if it seems better to you, add some boolean build-arg environment variable like COQ_INSTALL_SERAPI ?

Let me know if you need more input before opening your PR.