Ssreflect Users Discussion List

For what it is worth I've been using:

/nix/store/y6bghbgzphihml4pwf1lpihahilcj3nl-ocaml-3.12.1
/nix/store/sar69j83z5s0f7bazj46m2zgpbm1b4ng-camlp5_transitional-6.02.3
/nix/store/wfs04pcxxw2yyggwczk21bvyll3nyg0y-coq-8.4

to build ssreflect.  I don't know what variations are acceptable.

On Thu, 6 Sep 2012, Christian Doczkal wrote:

> I tried again, this time with camlp5-6.06 in tranistional mode.
>
> I recompiled Coq 8.4, this works just fine but the deprecated syntax
> errors for ssreflect remain.
>
> Regards
> Christian
>
>
> Am Donnerstag, den 06.09.2012, 10:42 +0200 schrieb Christian Doczkal:
> > Hi
> >
> > Thanks for the pointer. The problem affects my home machine which I cannot 
> > access at the moment. The gentoo ebuild appears to override the default and 
> > compile camlp5 in strict mode. I'll report later this evening whether this 
> > fixes the problem.
> >
> > Regards
> > Christian
> >
> >
> >
> >
> > On 06.09.2012, at 00:24,  wrote:
> >
> > > what does
> > >
> > > camlp5 -pmode
> > >
> > > output?
> > >
> > > AFAIU you require camlp5 to be built in transitional mode rather than strict mode 
> > > <http://pauillac.inria.fr/~ddr/camlp5/doc/html/strict.html>.
> > >
> > > On Thu, 6 Sep 2012, Christian Doczkal wrote:
> > >
> > > > Hello
> > > >
> > > > I have trouble building the contents of
> > > >
> > > >         ssreflect-1.4-coq8.4.tar.gz
> > > >
> > > > When I unpack the source and run make I get the following errors:
> > > >
> > > > File "src/ssrmatching.ml4", line 889, characters 0-7:
> > > > Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead
> > > > Preprocessing error on file src/ssrmatching.ml4
> > > >
> > > > ...
> > > >
> > > > File "src/ssreflect.ml4", line 481, characters 0-7:
> > > > Parse error: Deprecated syntax, use EXTEND MyGramModule ... END instead
> > > > Preprocessing error on file src/ssreflect.ml4
> > > >
> > > > Here are the program versions I use:
> > > >
> > > > $ coqc --version
> > > > The Coq Proof Assistant, version 8.4 (September 2012)
> > > > compiled on Sep 05 2012 22:28:55 with OCaml 3.12.1
> > > > $ camlp5 -v
> > > > Camlp5 version 6.02.3 (ocaml 3.12.1)
> > > >
> > > > OS: Gentoo Linux
> > > >
> > > > Remark: I recompiled everything using camlp5 6.06 but this didn't help
> > > >
> > > > Can someone tell me what I'm doing wrong? Any help would be appreciated.
> > > >
> > > > Regards
> > > > Christian
> > >
> > > --
> > > Russell O'Connor                                      <http://r6.ca/>
> > > ``All talk about `theft,''' the general counsel of the American Graphophone
> > > Company wrote, ``is the merest claptrap, for there exists no property in
> > > ideas musical, literary or artistic, except as defined by statute.''

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''