192522 2007-09-14 16:04 0000 sci-mathematics/coq-8.1 version bump request 2007-09-30 10:18:36 0000 1 1 1 Unclassified Gentoo Linux Applications unspecified All Linux RESOLVED FIXED P2 enhancement --- 1 pilki@melix.net sci@gentoo.org ml@gentoo.org pilki@melix.net 2007-09-14 16:04:11 0000 Version 8.1 of the Coq proof assistant is now the new stable version (http://coq.inria.fr/) Reproducible: Always markusle@gentoo.org 2007-09-29 15:46:34 0000 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 aballier@gentoo.org 2007-09-29 15:55:09 0000 (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 ! markusle@gentoo.org 2007-09-30 10:18:36 0000 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.