coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coqdoc - not a bytecode executable file

From: Xavier Leroy <Xavier.Leroy AT inria.fr>
To: "Richard W.M. Jones" <rjones AT redhat.com>
Cc: Stephane Glondu <steph AT glondu.net>, Mateusz Malinowski <m4linka AT gmail.com>, coq-club AT pauillac.inria.fr, amdunn AT gmail.com
Subject: Re: [Coq-Club] Coqdoc - not a bytecode executable file
Date: Wed, 03 Sep 2008 19:46:27 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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

Re: [Coq-Club] Coqdoc - not a bytecode executable file, Stephane Glondu
- Re: [Coq-Club] Coqdoc - not a bytecode executable file, Richard W.M. Jones
  - Re: [Coq-Club] Coqdoc - not a bytecode executable file, Alan Dunn
    - Re: [Coq-Club] Coqdoc - not a bytecode executable file, Richard W.M. Jones
  - Re: [Coq-Club] Coqdoc - not a bytecode executable file, Xavier Leroy
    - Re: [Coq-Club] Coqdoc - not a bytecode executable file, Stéphane Glondu