Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page