coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Latest Coq Git fails to build, Edward Z. Yang, 12/20/2012
- Re: [Coq-Club] Latest Coq Git fails to build, Hugo Herbelin, 12/20/2012
- Re: [Coq-Club] Latest Coq Git fails to build, Edward Z. Yang, 12/20/2012
- Re: [Coq-Club] Latest Coq Git fails to build, Pierre Letouzey, 12/21/2012
- Re: [Coq-Club] Latest Coq Git fails to build, Edward Z. Yang, 12/22/2012
- Re: [Coq-Club] Latest Coq Git fails to build, Pierre Letouzey, 12/21/2012
- Re: [Coq-Club] Latest Coq Git fails to build, Edward Z. Yang, 12/20/2012
- Re: [Coq-Club] Latest Coq Git fails to build, Hugo Herbelin, 12/20/2012
Archive powered by MHonArc 2.6.18.