coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Where to put csdp executable so that psatz finds it?

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Where to put csdp executable so that psatz finds it?
Date: Sat, 2 Jun 2018 21:25:03 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay2-d.mail.gandi.net
Ironport-phdr: 9a23:tY49IhJdZ2OCgoRfF9mcpTZWNBhigK39O0sv0rFitYgeKfjxwZ3uMQTl6Ol3ixeRBMOHs68C07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwVFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhjoZOT438G/ZicJ+g6xUrx2juxNxzJXZYJ2WOfdkYq/RYd0XSGpHU81MVyJBGIS8b44XAuQAJ+lfs5X9qEEIrRSmBAesBefvxSRWiX/swa0xzuMsEQ7c0wM+A9IBqnLUoM/6NKcTVeC617fHzS/fb/5Nwjf964jJcgsiofGNWLJwdNTeyVM1GwPDkFqQtZXoMjWI3eoDtGib6vBvVeOpi2M/pAFxoySvxscxiobSnI4a1lfE9SBhzIY0I924VFB0Ydq+HJRNqS6XMZZ9TMA6Q2xwpio2178LtYS5cSQW0pgr2h3SZvKdf4SV5h/uW/6dLDR7iX5/Zb6yhAi+/VKux+HgTMW53lRHoyxYmdfWrH8NzQbc6s2fR/t94Eih3TGP2hjJ6u5aJUA7j6raJ4A4zrEtjJYTtF7MHi7ymEnsg6+ZbEMk9fWp6+j9ZLXpuIOcO5d1igH4LKsuhtSyDfolPgUMRWSW+/iw2Kf+8UD6TrhGlOA6n63WvZzCIMQUvK+5Awtb0oY57Ba/Ci+r0NsCknYZMFJKYhSHg5LmO1HPJPD3Fumwg06wkDpw3PDGPb3gAo7OLnjClbfheKhy61RGxAo1099f+4pYCqsdL/LrRk/xqNvYAwclPAyz2ubrEcly1ocDWW2UGaKZK6PTsVqQ5u01OeWMZYkVuCz8K/c//fLug2U5yhchevyi2oJSY3SlFNxnJV+YaDzimIQvC2AP6yU3z/DjjmqtUDpZamyuF/Yz7zwnAYTgAobHTI23nJSa3zagHZxTY21cTFaBDSG7JM2/R/4QZXfKcYdamTseWO35Et5z5VSVrAb/joFfAK/R8ywcu4jk0YErtfbQhAox9DlxAt7b1WyRHTgtwjE4AgQu1aU6mnRTj0+Z2PEm0edbBMdQ5vZMXx18M5PAnbQjVoLCHznZd9LMc26IB9WrBTZrE4ArztsHchw4F5OnhxHHmSWjBbMU0bqGGM5s/w==

This is probably an issue with Coq looking for csdp but windows has csdp.exe
If replacing https://github.com/coq/coq/blob/04756f75bf54b1ccda8c180c62b14c5eaaaabb67/plugins/micromega/coq_micromega.ml#L2185 with

if System.is_in_system_path ("csdp" ^ Coq_config.exec_extension)

works then I'm right and you can make a PR (I don't have windows to test so not doing it myself)

Gaëtan Gilbert

On 02/06/2018 21:04, Soegtrop, Michael 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

[Coq-Club] Where to put csdp executable so that psatz finds it?, Soegtrop, Michael, 06/02/2018
- Re: [Coq-Club] Where to put csdp executable so that psatz finds it?, Gaëtan Gilbert, 06/02/2018
  - RE: [Coq-Club] Where to put csdp executable so that psatz finds it?, Soegtrop, Michael, 06/03/2018
    - Re: [Coq-Club] Where to put csdp executable so that psatz finds it?, Jason Gross, 06/04/2018
      - RE: [Coq-Club] Where to put csdp executable so that psatz finds it?, Soegtrop, Michael, 06/04/2018
- Re: [Coq-Club] Where to put csdp executable so that psatz finds it?, mukesh tiwari, 06/05/2018
  - RE: [Coq-Club] Where to put csdp executable so that psatz finds it?, Soegtrop, Michael, 06/05/2018