Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Extracting current proof state via Isabelle/Scala

Email Gateway (Mar 10 2025 at 17:39):

From: Milan Tom <mt904@cam.ac.uk>
Dear all,

If I have a headless session and directly update the document with some edits, how can I retrieve the current proof state of the document using Isabelle/Scala? For context, I am implementing a REPL to interact with Isabelle and this is the sort of function that I want to implement:

def step(isar_string: String): String = {
   println(session.tmp_dir_name)
   val node_name = Document.Node.Name("Test", theory = "Test")
   val edit = Text.Edit.insert(insertionPoint, isar_string)
   val node_edits = List((node_name, Document.Node.Edits[Text.Edit, Text.Perspective](List(edit))))

   session.update(Document.Blobs.empty, node_edits)
   val snapshot = session.await_stable_snapshot().switch(node_name)
   snapshot.node.source
}

This function seems to update the source correctly but I am unsure how to output the current proof state for a given node. I have tried:

   println(snapshot.messages)
   println(
     snapshot.node.commands.foreach(command =>
       println(snapshot.command_results(command))
     )
   )

This is just outputting an empty list of messages and empty results for each command.

Kindest regards,
Milan Tom

Last updated: Apr 17 2025 at 20:22 UTC