coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
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
Archive powered by MHonArc 2.6.18.