The Coq mailing list

["Alan Dunn" <amdunn AT gmail.com>]

I'm the Coq package maintainer for Fedora.

I was surprised to hear this, as this is something I explicitly
checked for (stripping vs. non-stripping of the binaries), so I
checked it again. I did receive the classic "No bytecode file
specified." error originally, which is a sign of problems along the
line you are suggesting. (I'm not sure your error is of this form
however... if you run just "coqdoc", what output do you get? If you
get a version number and compile time, eg:

This is coqdoc version 8.1pl3, compiled on Aug 05 2008 22:03:29

I would think it's not a stripping problem with coqdoc itself at
minimum.) However, when I reinstalled the package, things worked fine
(I ran coqdoc on RecTutorial.v, which produced an output HTML and CSS
file.)

I'm currently going to have to go with one of the explanations given
by Richard - at minimum it seems to work on install on Fedora 9,
though I'll try it on more than one machine again today to make sure I
didn't break anything with a further release (in going to release 3 of
my package). You will note as he said though that I have never tried
anything with Fedora 7 - the package is for Fedora >= 8. I'll look
into the possibility of the cronjob as an explanation for files that
were originally not stripped becoming so later on.

Profuse apologies for any problems.

- Alan

On Wed, Sep 3, 2008 at 6:04 AM, Richard W.M. Jones 
<rjones AT redhat.com>
 wrote:
> 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
>