FS#57905 - [coq] should optdepend on coin-or-csdp
Attached to Project:
Community Packages
Opened by Andres (andreser) - Tuesday, 20 March 2018, 22:06 GMT
Last edited by Baptiste (zorun) - Thursday, 03 May 2018, 07:21 GMT
Opened by Andres (andreser) - Tuesday, 20 March 2018, 22:06 GMT
Last edited by Baptiste (zorun) - Thursday, 03 May 2018, 07:21 GMT
|
Details
A plugin (psatz) that ships with Coq in package coq depends
on csdp. I have confirmed that it works when package
coin-or-csdp is installed. It may make sense to add
coin-or-csdp as an optional dependency of coq. Or perhaps as
a real dependency -- csdp+blas+lapack is around 3% of the
size of coq.
Example file that can be processed iff csdp is installed: Require Import ZArith Psatz. Lemma quadratic_Z a c b x (H : (a * x ^ 2 + b * x + c = 0)%Z) : (b ^ 2 >= 4 * a * c)%Z. psatz Z. Qed. Note that coq caches queries to csdp in .csdp.cache and uses information from that file even if csdp is not installed. |
This task depends upon
Closed by Baptiste (zorun)
Thursday, 03 May 2018, 07:21 GMT
Reason for closing: Fixed
Additional comments about closing: Fixed in coq 8.8.0-2
Thursday, 03 May 2018, 07:21 GMT
Reason for closing: Fixed
Additional comments about closing: Fixed in coq 8.8.0-2
If you have other dependency suggestions for other plugins please tell me.