Package Details: mathcomp 1.9.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: None
Last Packager: wilbowma
Votes: 6
Popularity: 0.000000
First Submitted: 2015-01-29 04:29
Last Updated: 2019-06-30 04:57

Dependencies (1)

Required by (0)

Sources (1)

Latest Comments

wilbowma commented on 2018-04-12 15:35

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

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

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

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

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

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).