Is coinor-csdp (the backend of psatz) something that could be considered for the Coq Platform? It seems pretty stable, useful, but so niche it's not packaged everywhere (I haven't investigated fully)
"no" is a perfectly acceptable answer, but a colleague noticed that even the following needs psatz, not just lra:
q1, q : Q H : 0 <= q1 ∧ q1 <= 1 H0 : 0 < q H1 : 0 < q * q1 H2 : ¬ 0 < q * (1 - q1) ============================ q1 == 1
FTR, there is a plan to add stuff to the current platform in the coming months (after fixing the Mac installer). @Michael Soegtrop is the one to talk to for more info.
This topic was moved here from #Coq users > psatz and coinor-csdp by Théo Zimmermann
Last updated: Jan 30 2023 at 11:03 UTC