Bug 704928 – sci-mathematics/coq-8.9.1-r1 - src_configure(): Num library not installed, required for OCaml 4.06 or later

• Product: Gentoo Linux
• Status: RESOLVED FIXED

[Description Artem Shinkarov 2020-01-07 13:45:43 UTC]

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.

[Comment 1 Jeroen Roovers (RETIRED) 2020-01-07 15:18:50 UTC]

Please attach the entire build log to this bug report.
Please post your `emerge --info' output in a comment.

[Comment 2 Artem Shinkarov 2020-01-07 15:28:24 UTC]

Created attachment 602756 [details]
emerge --info

As requested

[Comment 3 Artem Shinkarov 2020-01-07 15:28:45 UTC]

Created attachment 602758 [details]
build.log

[Comment 4 Larry the Git Cow 2020-01-07 21:00:59 UTC]

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 <[e-mail]>
AuthorDate: 2020-01-07 20:57:56 +0000
Commit:     Jason A. Donenfeld <[e-mail]>
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 <[e-mail]>

 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 <[e-mail]>
AuthorDate: 2020-01-07 20:54:51 +0000
Commit:     Jason A. Donenfeld <[e-mail]>
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 <[e-mail]>

 dev-ml/num/Manifest       |  1 +
 dev-ml/num/metadata.xml   |  5 +++++
 dev-ml/num/num-1.3.ebuild | 24 ++++++++++++++++++++++++
 3 files changed, 30 insertions(+)

[Comment 5 Sergio Perez 2020-01-07 23:36:16 UTC]

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.

[Comment 6 Artem Shinkarov 2020-01-08 08:38:19 UTC]

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.

[Comment 7 Artem Shinkarov 2020-01-08 08:43:15 UTC]

Larry, could you please push the camlp5 eubuild and update the dependency version of camlp5 in the coq ebuild?

[Comment 8 Artem Shinkarov 2020-01-08 08:44:53 UTC]

Sorry, Larry is a bot, I meant Jeroen :)

[Comment 9 Maciej Barć 2022-01-28 02:28:21 UTC]

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