Package Details: mathcomp 1.12.0-1

Git Clone URL: (read-only, click to copy)
Package Base: mathcomp
Description: The entire mathematical components library for Coq.
Upstream URL:
Licenses: GPL
Conflicts: ssreflect
Submitter: wilbowma
Maintainer: ormolu
Last Packager: ormolu
Votes: 6
Popularity: 0.000000
First Submitted: 2015-01-29 04:29 (UTC)
Last Updated: 2021-06-07 21:18 (UTC)

Dependencies (1)

Required by (0)

Sources (1)

Latest Comments

wilbowma commented on 2018-04-12 15:35 (UTC)

Thanks for the report! I'll try to patch the PKGBUILD and file a bug upstream if necessary.

xunam commented on 2018-04-12 13:50 (UTC)

I have the same problem as pruvisto, trying to build the package today with coq version 8.7.2-1. Apparently coq_makefile does not generate Makefile.coq.conf correctly and puts an incorrect value in the COQMF_WINDRIVE variable.

A quick fix consists in creating a file Makefile.coq.local next to Makfile.coq that contains 'COQMF_WINDRIVE =' (to make the variable empty).

I got a working package by doing this by hand and repacking with "makepkg -Rf" but I am not fluent enough in pkgbuild to write a patch to automate that. Actually, the proper fix would be to fix coq_makefile instead.

pruvisto commented on 2018-03-14 14:46 (UTC)

For me at least, this package seems to put mathcomp into "/user-contrib/mathcomp/" (yes, that is an absolute path!) instead of "/usr/lib/coq/user-contrib/mathcomp/".

I'm not sure why this happens.

zorun commented on 2017-02-09 19:20 (UTC)

The strange thing is that the -j argument seems to be ignored (both the one defined in /etc/makepkg.conf and the one explicitly given to make in the PKGBUILD). So, the package currently builds on a single core even with the -j3 you added. Also, ocaml-findlib should be in makedepends, not depends.

wilbowma commented on 2017-02-08 22:00 (UTC)

Will update shortly. I think the project used to recommend against parallel build; however, the docs now suggest -j 3 so I'll update that.

zorun commented on 2017-02-05 14:59 (UTC)

This package needs ocaml-findlib as a make dependency. Also, for some reason, there seems to be absolutely no parallelism in the build (i.e. it only ever uses one CPU core, and thus takes a really long time to build).