Re: Coq 8.0pl1 et ocaml 3.08.1
On Fri, Aug 20, 2004 at 01:51:52PM +0200, Michel Mauny wrote:
> Bonjour,
>
> [ English summary: here is a patch fixing Coq 8.0pl1 for it to compile
> under OCaml 3.08.1. ]
English Summary: thankingMichel for the patch :)
> On ne peut pas recompiler Coq 8.0 avec OCaml 3.08.1 à cause d'un bug
> Camlp4 que j'ai réparé dans cette dernière version.
>
> Les erreurs sont limitées à contrib/funind/tacinv.ml4 qui utilise des
> expressions OCaml du style
>
> fun x,y,z -> e
>
> voire même
>
> fun acc x,y -> e
>
> qui sont illégales en OCaml mais ont été acceptées par erreur par
> Camlp4 jusqu'à 3.08.0 incluse.
>
> Vous trouverez ci-joint un patch qui permet la compilation de Coq.
>
> J'aurai appris dans cette affaire que réparer des bugs dans une
> "bugfix release" n'est pas toujours une bonne idée (disons qu'il faut
> recompiler Coq avant de commit-ter les bugfixes).
>
> Désolé pour ces ennuis. Amicalement,
Merci, Michel. Je pense qu'avec les informations de Claudio on aurait
peut-etre pus reparer nous meme, mais c'est toujours plus agreable d'avoir des
patches directement. Cela veut probablement dire que nous pouvons uploader
3.08.1 et la nouvelle version de coq aussitot que alioth est reparer de
nouveau, donc soit aujourd'hui soit demain.
Amicalement,
Sven Luther
Reply to: