The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Hi Micheal,

This is just hunch because I don't have windows machine. I tried this on Linux and it's working fine.  I have downloaded the Csdp [1], and added it to my path

u5935541@newport:~$ echo $PATH
/home/users/u5935541/.opam/4.06.0/bin:/usr/lib/jvm/java-8-openjdk-amd64/:/home/users/u5935541/Mukesh/satsolvers/csdp6.2.0linuxx86_64/bin:/home/users/u5935541/Mukesh/racket/bin:/home/users/u5935541/bin:/home/users/u5935541/Mukesh/Excercism/bin:/home/users/u5935541/Mukesh/satsolvers/cvc4:/home/users/u5935541/Mukesh/clojure:/home/users/u5935541/Mukesh/satsolvers/yices-2.5.2/bin:/home/users/u5935541/Mukesh/satsolvers/mathsat-5.4.1-linux-x86_64/bin:/home/users/u5935541/Mukesh/satsolvers/boolector-2.4.1-with-lingeling-bbc/boolector/bin:/home/users/u5935541/Mukesh/HOL/bin:/home/users/u5935541/Mukesh/polyml/bin:/home/users/u5935541/.local/bin:/home/users/u5935541/Mukesh/satsolvers/z3satsolver/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games

You have already said that you can add it to the path, so my next hunch is if you are using Emacs then  M-x eshell should give you  (Any other editor should also import the executable path in its environment)

Welcome to the Emacs shell

~ $ echo $PATH
/home/users/u5935541/.opam/4.06.0/bin:/home/users/u5935541/.opam/4.06.0/bin:/usr/lib/jvm/java-8-openjdk-amd64/:/home/users/u5935541/Mukesh/satsolvers/csdp6.2.0linuxx86_64/bin:/home/users/u5935541/Mukesh/racket/bin:/home/users/u5935541/bin:/home/users/u5935541/Mukesh/Excercism/bin:/home/users/u5935541/Mukesh/satsolvers/cvc4:/home/users/u5935541/Mukesh/clojure:/home/users/u5935541/Mukesh/satsolvers/yices-2.5.2/bin:/home/users/u5935541/Mukesh/satsolvers/mathsat-5.4.1-linux-x86_64/bin:/home/users/u5935541/Mukesh/satsolvers/boolector-2.4.1-with-lingeling-bbc/boolector/bin:/home/users/u5935541/Mukesh/HOL/bin:/home/users/u5935541/Mukesh/polyml/bin:/home/users/u5935541/.local/bin:/home/users/u5935541/Mukesh/satsolvers/z3satsolver/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games
~ $

And I can discharge this proof
 

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.

Best regards,

Mukesh Tiwari

[1] https://projects.coin-or.org/Csdp/

On Sun, Jun 3, 2018 at 5:04 AM, Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

Dear Coq Users / Team

 

I wanted to give psatz a try, which requires the external csdp solver. The binary can be downloaded and I put it somewhere such that it is in the path, but psatz doesn’t find it. I wonder where to put csdp (on Windows), so that it is found by psatz.

 

Best regards,

 

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928