The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

On Wed, Jul 25, 2012 at 2:26 PM, Stéphane Glondu <steph AT glondu.net> wrote:

Le 24/07/2012 15:46, Beta Ziliani a écrit :

> I can create a new coq toplevel with the usual coqmktop command without
> any issues. Now, when I add the "-top" option, compilation breaks with
> the following message:
>
>
> $ ~/coq-8.4beta2/bin/coqmktop.byte -g -top  -o coqtop src/run.cmo
> src/runtac.cmo
>

> File "/tmp/coqmain4bdbf3.ml <http://coqmain4bdbf3.ml>", line 15,

> characters 57-67:
> Error: Unbound module Util
>
> I compiled coq with the options "-debug" and "-local".
>
> Any suggestions on how to fix this?

This is a bug in coqmktop. Please file a bug report.

My guess is that your command works if you configure coq without -local.

Thanks for the suggestion, but it still doesn't work. I have some 8.4 trunk version from February 2012 installed in the system, and coqmktop -top fails in the exact same way.

Best,
Beta
 

Cheers,

--
Stéphane