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

mathcomp for coq-8.9 #1

Closed CohenCyril closed 5 years ago

CohenCyril commented 5 years ago

Hi @erikmd I thought you said somewhere there was a reason for not having a docker build for mathcomp on coq 8.9, could you remind me what it is?

erikmd commented 5 years ago

Hi @CohenCyril, the only missing ingredient is an opam release for bignums (coq/bignums#17). There is now a pending PR coq/opam-coq-archive#568, so as soon as it is merged I'll publish the corresponding image in coqorg/coq then in mathcomp/mathcomp.

erikmd commented 5 years ago

done: docker run --rm -it mathcomp/mathcomp:1.7.0-coq-8.9 rlwrap coqtop