The error message says: Num library not installed, required for OCaml 4.06 or later I guess it refers to: https://github.com/ocaml/num/ But we don't have a package for this library! I'll leave it in the hands of the ebuild maintainer to decide whether we need to add this library or to hardcode library pulling into coq compilation. Generally, seems like an easy fix.
Please attach the entire build log to this bug report. Please post your `emerge --info' output in a comment.
Created attachment 602756 [details] emerge --info As requested
Created attachment 602758 [details] build.log
The bug has been closed via the following commit(s): https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=a41e99d5d07a2fafd4f7bab90567ed25fe5306d7 commit a41e99d5d07a2fafd4f7bab90567ed25fe5306d7 Author: Jason A. Donenfeld <zx2c4@gentoo.org> AuthorDate: 2020-01-07 20:57:56 +0000 Commit: Jason A. Donenfeld <zx2c4@gentoo.org> CommitDate: 2020-01-07 21:00:55 +0000 sci-mathematics/coq: revbump for newer ocaml + num Fixes: https://bugs.gentoo.org/704928 Package-Manager: Portage-2.3.84, Repoman-2.3.20 Signed-off-by: Jason A. Donenfeld <zx2c4@gentoo.org> sci-mathematics/coq/coq-8.9.1-r2.ebuild | 86 +++++++++++++++++++++++++++++++++ 1 file changed, 86 insertions(+) https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=0849f2d4192c441bdd07a752b02c780b5a8b3022 commit 0849f2d4192c441bdd07a752b02c780b5a8b3022 Author: Jason A. Donenfeld <zx2c4@gentoo.org> AuthorDate: 2020-01-07 20:54:51 +0000 Commit: Jason A. Donenfeld <zx2c4@gentoo.org> CommitDate: 2020-01-07 21:00:55 +0000 dev-ml/num: add for newer ocaml + coq Fixes: https://bugs.gentoo.org/704928 Package-Manager: Portage-2.3.84, Repoman-2.3.20 Signed-off-by: Jason A. Donenfeld <zx2c4@gentoo.org> dev-ml/num/Manifest | 1 + dev-ml/num/metadata.xml | 5 +++++ dev-ml/num/num-1.3.ebuild | 24 ++++++++++++++++++++++++ 3 files changed, 30 insertions(+)
Hi, it seems you added dev-ml/num as a dependency for the current coq version sci-mathematics/coq-8.9.1-r2 dev-ml/ocaml-4.05.0-r1 installs the same files as dev-ml/num-1.3 would, therefore there is a collision. if I now update to dev-ocaml-4.09.0 I can install dev-ml/num-1.3 but dev-ml/camlp5-7.03, another dependency does not build with this version it gives: Sorry: the compatibility with ocaml version "4.09.0" is not yet implemented. Please report.
Created attachment 602770 [details] Version bump fo camlp5 that works with ocaml 4.9.0 Sergio, have a look at the attached ebuild for the camlp5. It is just a trivial version bump, and it seem to work fine for me. The original camlp5 is a few versions behind the latest one.
Larry, could you please push the camlp5 eubuild and update the dependency version of camlp5 in the coq ebuild?
Sorry, Larry is a bot, I meant Jeroen :)
8.9 is no longer in the tree. Seems like this commit closed (should close) it: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=a41e99d5d07a2fafd4f7bab90567ed25fe5306d7
