Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Latest Coq Git fails to build

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Latest Coq Git fails to build


Chronological Thread 
  • From: Hugo Herbelin <Hugo.Herbelin AT inria.fr>
  • To: "Edward Z. Yang" <ezyang AT MIT.EDU>
  • Cc: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Latest Coq Git fails to build
  • Date: Thu, 20 Dec 2012 08:22:31 +0100

Option -rectypes should no longer be needed. You probably have an old
mltop.cmx around and you need to regenerate the dependencies
files. Did you "make clean"?

Hugo Herbelin

On Thu, Dec 20, 2012 at 02:39:51PM +0800, Edward Z. Yang wrote:
> Hey all,
>
> I'm getting this error when I'm trying to build the latest Coq from Git:
>
> cd kernel/byterun/ && \
> "ocamlmklib" -oc coqrun coq_fix_code.o coq_memory.o coq_values.o
> coq_interp.o
> COQMKTOP -o bin/coqtop
> File "/tmp/coqmain54c3cb.ml", line 1, characters 0-1:
> Error: Unit Coqmain54c3cb imports from Mltop, which uses recursive types.
> The compilation flag -rectypes is required
> make[1]: *** [bin/coqtop] Error 2
> make[1]: Leaving directory `/srv/code/coq-git'
> make: *** [world] Error 2
>
> Anyone know what's up? Should I file a bug?
>
> Cheers,
> Edward



Archive powered by MHonArc 2.6.18.

Top of Page