Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club]Compilation error in coqide (8.1)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]Compilation error in coqide (8.1)


chronological Thread 
  • From: Samuel Mimram <samuel.mimram AT ens-lyon.org>
  • To: Edsko de Vries <devriese AT cs.tcd.ie>
  • Cc: Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>, coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club]Compilation error in coqide (8.1)
  • Date: Fri, 09 Mar 2007 14:54:38 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
  • Organization: PPS

Hi,

Edsko de Vries wrote:
> On Thu, Mar 08, 2007 at 06:21:02PM +0100, Pierre Letouzey wrote:
>> On Thu, Mar 08, 2007 at 05:05:48PM +0000, Edsko de Vries wrote:
>>>
>>> When I try to compile coq 8.1 with the IDE enabled, I get the following
>>> compilation error:
>> Hi
>>
>> This looks like a small configure bug I've already encountered after
>> the release of 8.1 and fixed in the svn version. With your 8.1, the
>> bug can be easily bypassed without any patch: simply run ./configure
>> again but this time **without** any flag concerning coqide (the
>> -coqide flag is not mandatory anyway since the default behavior of
>> ./configure is to compile coqide if it finds a suitable lablgtk2).
> 
> Yep, that did it. Thanks! I created a simple Debian package for Coq 8.1;
> I don't know who is maintaining the "official" package, or how long it
> takes for these things to propagate into Debian testing, but if that is
> a slow process, perhaps it would be useful if I put that package up
> somewhere?

An official package is already available for Debian in the experimental
section, see http://packages.debian.org/experimental/math/coq
It will be available in unstable (and soon after, in testing) when the
new stable version of Debian is released. For now, package propagation
is mostly frozen.

Cheers,

Samuel.





Archive powered by MhonArc 2.6.16.

Top of Page