search

math-comp / docker-mathcomp

Docker images of coq-mathcomp [maintainer=@erikmd]
https://hub.docker.com/r/mathcomp/mathcomp/#supported-tags
BSD 3-Clause "New" or "Revised" License
6 stars 2 forks source link

coq-dev docker images seem broken #29

Closed JasonGross closed 1 year ago

JasonGross commented 1 year ago

I'm getting

Pull docker image
  COQ_IMAGE=mathcomp/mathcomp:1.17.0-coq-dev

  Error response from daemon: No such image: mathcomp/mathcomp:1.17.0-coq-dev
  Error response from daemon: manifest for mathcomp/mathcomp:1.17.0-coq-dev not found: manifest unknown: manifest

at https://github.com/JasonGross/neural-net-coq-interp/actions/runs/6738411252/job/18317928200?pr=6#step:5:221

erikmd commented 1 year ago

Hi @JasonGross, this image is not available anymore, because mathcomp 1.17.0 fails to build from source with coq-dev, see e.g.: https://github.com/coq/opam/commit/c0825ef0f571f037d92fefadfb911bcb4ef7fee2 https://gitlab.inria.fr/math-comp/docker-mathcomp/-/pipelines/875410

You can use these images instead: https://hub.docker.com/r/mathcomp/mathcomp/tags?page=1&name=coq-dev

erikmd commented 1 year ago

Still, it seems the documentation (https://hub.docker.com/r/mathcomp/mathcomp#supported-tags) needs an update to make this clearer. Will do this now.

erikmd commented 1 year ago

Thanks @JasonGross for your report!

Closed by 180b9f4659169d669b347d61e46d73e6ac5d5894