The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

On Tue, Dec 02, 2014 at 03:48:27PM -0500, Jonathan wrote:
> On 12/02/2014 05:28 AM, Georges Gonthier wrote:
> >   If you really need this particular feature, you might want to consider 
> > the Ssreflect plugin. Ssreflect tactics generally accept Coq integers 
> > along Caml ones; in particular it is possible to compute iteration counts 
> > (as in do N!tactic), occurrence selectors (set x := {+N}y), and subgoal 
> > selectors (tac1; first N [tacN]).
> >  -- Georges
> 
> I will try ssreflect.  I am using the trunk version of Coq, so I
> note that the latest ssreflect sources are at: 
> https://gforge.inria.fr/scm/viewvc.php/trunk/Saclay/Ssreflect/?root=coq-contribs.
> However - how is this downloaded?  It doesn't work to git clone that
> address, or use it as an svn source repository.

To compile a package on coq-contribs (for instance for
Saclay/Ssreflect), you can proceed as follows:

svn checkout 
svn://scm.gforge.inria.fr/svnroot/coq-contribs/trunk/Saclay/Ssreflect
cd Ssreflect
make
# to use locally:
coqtop -I src -R theories Ssreflect -require ssreflect  # or coqide, ...

This assumes that your default versions of ocaml/camlp5 are the same
as the ones you used to compile coq.

Remarks:

- With git, something like this (assuming Saclay/Ssreflect) should work:

  git svn clone svn://scm.gforge.inria.fr/svn/coq-contribs/Saclay/Ssreflect

- Notice that some contribs have dependencies. For instance, the
  Orsay/Ergo SMT solver depends on Orsay/Containers (type classes
  based finite maps et finite sets), Orsay/Counting and Orsay/Nfix
  (see file description in the archive).

- About the Saclay/Ssreflect package on coq-contribs: it does not only
  contain the "ssreflect" plugin (with Gonthier's tactics) and a
  couple of associated .v files. It also contains the formalized proof of
  the Feit-Thompson theorem and (a large part of) the Mathematical
  Components library (this is how the authors of the package submitted
  it to the coq-contribs).

- More generally, an opam-based system is being to be released soon
  which will support compiling and installing different combinations
  of versions of Coq, plugins and libraries consistently. However, at
  the current time, the ssreflect plugin is available only with Coq
  8.4.

- The trunk is the development version, so it is unstable and some coq
  contribs might not compile. Which contribs are compiling correctly is e.g.
  visible at http://coq.inria.fr/bench/coqbench.cgi?version=trunk (but
  to be subsumed soon by a new opam-based report). For instance, use
  e.g. e1e1a13b015e49 but not e2fa65fccb9d for Saclay/Ssreflect.

Hope it helps,

Hugo Herbelin