The Coq mailing list

["Richard W.M. Jones" <rjones AT redhat.com>]

On Wed, Sep 03, 2008 at 11:51:30AM +0200, Stephane Glondu wrote:
> Mateusz Malinowski a écrit :
>> I have a problem with Coqdoc, when I type coqdoc x.v then my bash will
>> inform me: 'Fatal error: the x.v is not a bytecode executable file'.
>> Apart from this if I type coqdoc --glob-from x.v I'll get 'Unknown
>> option --glob-from'. I'm wondering if someone had similar problems.
>
> This sounds like a stripped executable linked with -custom.
>
>> I'm currently using Fedora 7 and The Coq Proof Assistant, version
>> 8.1pl3 and I installed Coq from rpm.
>
> Did you install the Fedora package? If so, you should probably fill in a  
> bug report against the Fedora package.
>
> BTW, there is a beta available for the next version of Coq at:
>
>   http://coq.inria.fr/V8.2beta/
>
> There are also RPMs.

A few comments here:

(1) Don't file bugs in Bugzilla unless you're using Fedora RPMs.
AFAIK there are no Fedora Coq RPMs for Fedora 7 (which in any case
isn't a supported release of Fedora).  On the other hand, please do
try out a more up to date version of Fedora, the supported Coq, and
file any bugs as necessary.
  https://admin.fedoraproject.org/pkgdb/packages/name/coq
  http://bugzilla.redhat.com/

(2) The -custom option is deprecated in OCaml.  You wouldn't be
expected to know this because no one was told :-) but you can read
more about it here:
http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=256900#49

(3) Fedora has some cronjob which manages to damage executables that
have bytecode appended to them, by doing a kind of 'strip' on them.
We didn't really discover this until quite recently, and I've been
going through the repository to fix up the few executables which are
broken by this.  Hopefully because -custom is deprecated we can
persuade upstreams to make fixes too.

Rich.

-- 
Richard Jones, Emerging Technologies, Red Hat  http://et.redhat.com/~rjones
virt-top is 'top' for virtual machines.  Tiny program with many
powerful monitoring features, net stats, disk stats, logging, etc.
http://et.redhat.com/~rjones/virt-top