The Coq mailing list

[Ashish Darbari <ashish_darbariuk AT yahoo.co.uk>]

Hi Fellows,

I tried building Coq-8.2 and it fails. Any clue?

I've a Mac OSX Darwin, ocaml-3.10.2 and camlp5-5.10

both successfully installed from sources.

Thanks

Ashish

Prayag:/usr/local/coq-8.2beta4 root# make world

*****************************************************

*****************************************************

****************** Entering stage1 ******************

*****************************************************

*****************************************************

make -f Makefile.stage1 "stage1"

make[1]: Entering directory `/usr/local/coq-8.2beta4'

OCAMLC4   lib/compat.ml4

File "lib/compat.ml4", line 17, characters 11-25:

Unbound type constructor Stdpp.location

make[1]: *** [lib/compat.cmo] Error 2

make[1]: Leaving directory `/usr/local/coq-8.2beta4'

make: *** [stage1] Error 2

---

From: Stéphane Lescuyer <lescuyer AT lri.fr>
To: Adam Chlipala <adamc AT hcoop.net>
Cc: Ashish Darbari <ashish AT darbari.org>; coq-club AT pauillac.inria.fr
Sent: Sunday, 11 January, 2009 19:22:28
Subject: Re: [Coq-Club] Finite Maps

There was indeed a discussion about this issue earlier in December and
Pierre Letouzey pointed to a new command

Extraction Blacklist <module name> .... .

that forces the extraction mechanism to rename modules like List and
String, in order to avoid clashes with the usual OCaml modules.
That would solve your issue without resorting to -pack (or worse, to sed).
It is only available in the svn snapshot or the current 8.2 beta version though.

HTH,

Stéphane L.


On Sun, Jan 11, 2009 at 8:12 PM, Adam Chlipala <adamc AT hcoop.net> wrote:
> Ashish Darbari wrote:
>>
>> However having compiled these using ocaml compilers and loading (#use)
>>
>> the fMapAVL.ml I get an error message
>>
>> The file ocaml and fMapList.cmi make inconsistent assumptions over
>> interface List
>>
>
> I expect that you extracted a file list.ml, which conflicts with [List] from
> the OCaml standard library.  Check out the [-pack] option to the OCaml
> compilers for a way to put your extracted modules in a separate namespace
> and avoid the clash.
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>        http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>



--
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06