The Coq mailing list

[Pierre Letouzey <pierre.letouzey AT inria.fr>]

Hi

Your error message mentions Mltop, that recently changed of status:
it used to be a .ml4, it is now a basic .ml (and certainly does not
require -rectypes anymore). I suspect a mess around this mltop in
your repository, "make clean" isn't always perfect at removing
generated files, especially after a transition like this one.
Since you're using git, I suggest a "git clean -xfd" (caution:
this will *erase* any files unknown to git from this repository).

Hope this helps...

Pierre L.

----- Mail original -----
> Nope, I did a make clean, checked that there were no cmx files in my
> source
> directory, and still am getting build errors.
> 
> To be clear, I'm on this commit:
> 
> commit 787e409e773d45da6d149fbcdf9657b0be4a5529
> Author: pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>
> Date:   Wed Dec 19 22:34:35 2012 +0000
> 
>     Reductionops reduction machine can refold constant
>     
>     git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16107
>     85f007b7-540e-0410-9357-904b9bb8a0f7
> 
> Cheers,
> Edward
> 
> Excerpts from Hugo Herbelin's message of Thu Dec 20 15:22:31 +0800
> 2012:
> > 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
>