Search code examples
pythoncoqisabelle

How we can access Coq or Isabelle/HOL using python program?

I want to access Coq or Isabelle/HOL interactive theorem prover using my python program. Is there any python packages is available? Please suggest

Solution

  • This is a very rough draft of how to start an Isabelle instance and perform an RPC call from Python:

    import $ivy.`info.hupel::libisabelle-setup:0.9.2`
import $ivy.`org.python:jython-standalone:2.7.1`

import javax.script.ScriptEngineManager

val python = """
  |from info.hupel.isabelle.api import Configuration, Version
  |from info.hupel.isabelle.japi import JResources, JSetup, JSystem, Operations
  |res = JResources.dumpIsabelleResources()
  |print res
  |config = Configuration.simple("Protocol")
  |print config
  |env = JSetup.makeEnvironment(JSetup.defaultSetup(Version.Stable("2016-1")), res)
  |print env
  |sys = JSystem.create(env, config)
  |print sys
  |response = sys.invoke(Operations.HELLO, "world")
  |print response
  |sys.dispose()""".stripMargin

new ScriptEngineManager().getEngineByName("python").eval(python)

    This is wrapped in Scala code for the simple reason that this was the easiest way to get Jython working.

    To execute the script above, save it as a file (e.g. isa.sc), download the Ammonite REPL for Scala, and run it like ammonite isa.sc. This should then take a while to do some setup and finally, something like this should appear:

    info.hupel.isabelle.japi.JResources@59d0fac9
session Protocol
<Isabelle2016-1> at /home/lars/.local/share/libisabelle/setups/Isabelle2016-1
info.hupel.isabelle.japi.JSystem@138a952f
Hello world

    This demonstrates very simple Isabelle bootstrapping from Python.