Home | Docs | Forums | Lists | Bugs | Planet | Store | GMN | Get Gentoo!

Full Text Bug Listing

Version 8.1 of the Coq proof assistant is now the new stable version
(http://coq.inria.fr/)

Reproducible: Always

Thanks for the note and I've just bumped coq to 8.1pl1.

ml@g.o folks!

Unfortunately, coq-8.1pl1 badly fails to compile with ocaml-3.10.0;
the patch posted on the coq website for ocaml-3.10.0 doesn't seem
to work, but since I don't know ocaml at all it is hard to tell
for me at the moment what the problem is. I'll try to have a look at
it sometime but due to me not knowing ocaml at all this one may
be difficult to fix.

Thanks,
Markus

(In reply to comment #1)
> Unfortunately, coq-8.1pl1 badly fails to compile with ocaml-3.10.0;
> the patch posted on the coq website for ocaml-3.10.0 doesn't seem
> to work, but since I don't know ocaml at all it is hard to tell
> for me at the moment what the problem is. I'll try to have a look at
> it sometime but due to me not knowing ocaml at all this one may
> be difficult to fix.

imho don't waste your time doing this, it's definitely not a trivial thing to
fix and afaik upstream has been working on it. The patch posted is supposed to
be used with dev-ml/camlp5 but I've heard it still has issues with it. I'd say
just wait for a new release, ocaml 3.10 still has other issues that block its
unmasking, so one more or one less... And thanks for bumping coq !

Thanks much for your comments! I will wait then and please
don't hesitate to ping me if anything needs to be done
in the meantime.