coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Atb.: Coq API, call of Coq from external program

From: Alex Meyer <alex153 AT outlook.lv>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Atb.: Coq API, call of Coq from external program
Date: Mon, 4 Sep 2017 10:56:08 +0000
Accept-language: lv-LV, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=alex153 AT outlook.lv; spf=Pass smtp.mailfrom=alex153 AT outlook.lv; spf=Pass smtp.helo=postmaster AT EUR02-HE1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:UdfuNhafzEF7Zs3uNP3kEUn/LSx+4OfEezUN459isYplN5qZpsu+bnLW6fgltlLVR4KTs6sC0LWG9f24EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i76vnYuHUC1Pg1sY+/xB4T6jsKt1un09YeZK1FDgyP4ardvJj23qx/Qv48Ym90xBLw2z07gpnZYM8Fb1G5ybQaamxvsv5rr1Jl+7yBXvPFn89AWAvayRLgxUbENVGduCGsy/sC+7RQ=
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

I have already received good answer here:

https://stackoverflow.com/questions/46032067/how-to-call-proof-asistant-coq-from-external-software

That is already sufficient.

No: coq-club-request AT inria.fr <coq-club-request AT inria.fr> Alex Meyer <alex153 AT outlook.lv> vārdā
Nosūtīts: pirmdiena, 2017. gada 4. septembris 9:50
Kam: coq-club AT inria.fr
Tēma: [Coq-Club] Coq API, call of Coq from external program

Hi!

Does Coq have some API to call it from other programmas (Java, C++) and is it possible to integrate Coq into external worflow? Is there are no API, then it can be sufficient to call coq from command line and provide input in some some and get results in some other file. If that is possible?

Alex

[Coq-Club] Coq API, call of Coq from external program, Alex Meyer, 09/04/2017
- [Coq-Club] Atb.: Coq API, call of Coq from external program, Alex Meyer, 09/04/2017