Error message from Psatz crashes vscoq
Closed this issue · 4 comments
thery commented
With vscoq 2.0.3 and coq 8.18 in stepping mode , the following file
Require Import ZArith Psatz.
Open Scope Z_scope.
Goal 1 + 1 = 3.
Proof.
psatz Z 5.crashes when trying to apply psatz. When compiling the file with coqc we get the following error message :
% coqc foo.v
find_witness Micromega_plugin.Coq_micromega.CsdpNotFoundfind_witness Micromega_plugin.Coq_micromega.CsdpNotFoundFile "./foo.v", line 7, characters 0-10:
Error:
Tactic failure: Skipping the rest of this tactic: the complexity of the goal requires the use of an external tool called CSDP.
However, the "csdp" binary is not present in the search path.
Some OS distributions include CSDP (package "coinor-csdp" on Debian for instance). You can download binaries and source code from <https://github.com/coin-or/csdp>..
rtetley commented
What do you mean by crash ?
I get the following error:
Anomaly "Uncaught exception Unix.Unix_error(Unix.ENOENT, "create_process", "csdpcert")." Please report at http://coq.inria.fr/bugs/.
but the program does not crash ?
thery commented
I don't see the message and after the interface is dead : no interaction possible
rtetley commented
Closing. Feel free to reopen if this still happens