The Coq mailing list

["Edward Z. Yang" <ezyang AT MIT.EDU>]

I bet that's it.  Thanks for the pointer!

Edward

Excerpts from Pierre Letouzey's message of Fri Dec 21 22:06:41 +0800 2012:
> 
> 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
> >