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
Task Type Bug Report
Category Packages
Status Closed
Assigned To Baptiste (zorun)
Architecture All
Severity Very Low
Priority Normal
Reported Version
Due in Version Undecided
Due Date Undecided
Percent Complete 100%
Votes 0
Private No

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
Comment by Baptiste (zorun) - Wednesday, 21 March 2018, 21:35 GMT
Ok, I will add it to optdepends with the next update.

If you have other dependency suggestions for other plugins please tell me.

Loading...