Ssreflect Users Discussion List

[Yves Bertot <>]

Hello,

My competence in docker are limited, but strong enough to construct an 
image of an ubuntu system with one user
named johndoe, with an opam installation of coq 8.6.1 containing the 
whole of mathematical components 1.6.1 and
the complete proof of the odd order theorem as available as an opam package.


the repository is the following one:

https://hub.docker.com/r/ybertot/coq-with-libraries/

the two images provided so far are given by the following tags:

odd.order.1.6.1

mathcomp.1.6.1

Names should be self-explanatory.

The images were built thanks to build instructions that are visible in 
the following repository:

https://gitlab.inria.fr/bertot/coq-docker

At the time of writing these lines, I can't provide a short tutorial of 
how to use these images: you have to follow
the instruction provided by the docker tool, which needs to be installed 
on your machine.

With my best,

Yves