Stream: Coq Platform devs & users

Topic: psatz and coinor-csdp

view this post on Zulip Paolo Giarrusso (Jan 15 2021 at 01:33):

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)

view this post on Zulip Paolo Giarrusso (Jan 15 2021 at 01:37):

"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

view this post on Zulip Karl Palmskog (Jan 15 2021 at 07:22):

see: https://github.com/coq/platform/issues/39

Add csdp to the Coq Platform · Issue #39 · coq/platform
The psatz tactic uses the external tool csdp. To make it convenient for users of any platform to call psatz, I propose that csdp is included in the Coq Platform. Debian and Ubuntu users can already...

view this post on Zulip Karl Palmskog (Jan 15 2021 at 07:23):

also: https://coq.zulipchat.com/#narrow/stream/250632-Coq-Platform.20devs.20.26.20users/topic/csdp.20in.20the.20platform.3F

view this post on Zulip Enrico Tassi (Jan 15 2021 at 07:26):

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.

view this post on Zulip Notification Bot (Jan 15 2021 at 20:04):

This topic was moved here from #Coq users > psatz and coinor-csdp by Théo Zimmermann

Last updated: Oct 13 2024 at 01:02 UTC