Coqdoc - not a bytecode executable file

[Mateusz Malinowski]

Good afternoon,
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.

I'm currently using Fedora 7 and The Coq Proof Assistant, version
8.1pl3 and I installed Coq from rpm.

Best wishes,
M.M.

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Stéphane Glondu]

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.


Cheers,

--
Stéphane

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Richard W.M. Jones-2]

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

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Alan Dunn-3]

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@...> 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
>

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Richard W.M. Jones-2]

On Wed, Sep 03, 2008 at 06:33:25AM -0400, Alan Dunn wrote:
> 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.

You may be hitting the prelink stripping problem.  See:

https://www.redhat.com/archives/fedora-devel-list/2008-September/thread.html#00045

The easy answer is to drop a file in the /etc/prelink.conf.d/
directory containing one line for each file that you wish prelink not
to touch:

  -b /usr/bin/coq
  -b /usr/bin/coqdoc

(You can also use globs).

The prelink cronjob seems to run nightly, so you can have an RPM which
is protected from stripping, install it, and everything seems fine
until the next morning when you discover the binary is broken.

The whole concept of having cronjobs which modify installed binaries
is off the crack-radar IMHO.

Rich.

--
Richard Jones, Emerging Technologies, Red Hat  http://et.redhat.com/~rjones
virt-p2v converts physical machines to virtual machines.  Boot with a
live CD or over the network (PXE) and turn machines into Xen guests.
http://et.redhat.com/~rjones/virt-p2v

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Xavier Leroy]

> (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

Just to summarize my position:
1- quite often -custom is no longer needed (it's a leftover from
   the days before the OCaml bytecode interpreter could load DLLs
   containing C primitives);
2- there is an alternative (the DLL approach) that is generally better.

As a case in point, the Makefile for Coq 8.1 sets -custom while
compiling coqdoc, while I'm pretty sure it would work without.
(I didn't check 8.2, though.)

> The whole concept of having cronjobs which modify installed binaries
> is off the crack-radar IMHO.

I agree with you.

- Xavier Leroy

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Stéphane Glondu]

Xavier Leroy wrote:
> As a case in point, the Makefile for Coq 8.1 sets -custom while
> compiling coqdoc, while I'm pretty sure it would work without.
> (I didn't check 8.2, though.)

The issue is being worked on at the moment. Hopefully, 8.2 won't use
-custom anymore.


Cheers,

--
Stéphane Glondu


--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club