Tom Tom - 2 years ago 251
Python Question

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

Answer Source

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

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., download the Ammonite REPL for Scala, and run it like ammonite This should then take a while to do some setup and finally, something like this should appear:

session Protocol
<Isabelle2016-1> at /home/lars/.local/share/libisabelle/setups/Isabelle2016-1
Hello world

This demonstrates very simple Isabelle bootstrapping from Python.

Recommended from our users: Dynamic Network Monitoring from WhatsUp Gold from IPSwitch. Free Download