Public | Automated Build

Last pushed: a year ago
Short Description
Coq + Ssreflect/Mathcomp installed on an official opam image
Full Description

Current version:

  • Opam 1.2.2 / Ocaml 4.04.0
  • Coq 8.6
  • Ssreflect / Mathcomp (+ coq-mathcomp-algebra) 1.6.1
  • Emacs 24.5.1
  • ProofGeneral 4.3pre131011

To use interactively:

docker run --rm -ti --detach-keys "ctrl-l,l" -v $(pwd):/home/opam/work okuisatoshi/docker_coq_ssr emacs -nw work/yourfile.v

Or just log in:

docker run --rm -ti --detach-keys "ctrl-l,l" -v $(pwd):/home/opam/work okuisatoshi/docker_coq_ssr bash

To include Ssreflect modules, e.g.:

Require Import ssreflect ssrfun ssrbool ssrnat seq fintype matrix ...

Japanese users might prefer okuisatoshi/docker_coq_ssr_ja.

Docker Pull Command
Source Repository