Stream: General

Topic: tools to automatically adopt sledgehammer proofs into theory

Chengsong Tan (May 01 2024 at 21:22):

Hi all,

I am trying to find an automatic tools that helps you to copy-and-paste proofs found by sledgehammer into their invocation sites. Here's a screenshot for a typical workload:
Screenshot-2024-05-01-at-22.16.14.png
I am dealing with Isar proofs that are composed of hundreds of subgoals like these, most of which can be solved by sledgehammer with a one-liner proof. The problem is whether this copy-paste job can be totally automated so that I can focus only on the goals that needs human intervention. I am hoping there's some existing tools for this, but any suggestions/sources of information for implementing one would also be greatly appreciated.

Best wishes,
Chengsong

Fabian Huch (May 02 2024 at 06:56):

I don't know of an existing tool doing this. To build this, you'd have to define a Scala.Fun in Isabelle/Scala to perform the document edit, and then write your custom s/h command that invokes this function from the Isabelle/ML process (using the \<^scala> antiquotation) whenever a proof is found.

Chengsong Tan (May 02 2024 at 16:22):

Fabian Huch said:

I don't know of an existing tool doing this. To build this, you'd have to define a Scala.Fun in Isabelle/Scala to perform the document edit, and then write your custom s/h command that invokes this function from the Isabelle/ML process (using the \<^scala> antiquotation) whenever a proof is found.

Hi Fabian,

Thanks a lot for the reply!

If you have used Isabelle/Scala, could you give me some advice on setting things up and experiment with the tool? Right now I am trying to follow the very short tutorial on
https://dominique-unruh.github.io/scala-isabelle/setup.html, however I got the error

error:
  bad constant pool index: 0 at pos: 48461
     while compiling: <no file>
        during phase: globalPhase=<no phase>, enteringPhase=<some phase>
     library version: version 2.13.7
    compiler version: version 2.13.7
  reconstructed args: -d /var/folders/gp/sn8kdjh95bv3fq5315dv1bww0000gp/T/scalascript10668209491638361976.tmp

  last tree to typer: EmptyTree
       tree position: <unknown>
            tree tpe: <notype>
              symbol: null
           call site: <none> in <none>

by running scala Example.scala in https://dominique-unruh.github.io/scala-isabelle/example.html.

Fabian Huch (May 02 2024 at 16:30):

I have no Idea about scala-isabelle, I was referring to Isabelle/Scala, which is the Isabelle suprocess within the system. Isabelle/Scala is extensively documented in the system manual, Chapter 5.

Chengsong Tan (May 02 2024 at 17:55):

Fabian Huch said:

I don't know of an existing tool doing this. To build this, you'd have to define a Scala.Fun in Isabelle/Scala to perform the document edit, and then write your custom s/h command that invokes this function from the Isabelle/ML process (using the \<^scala> antiquotation) whenever a proof is found.

Hi Fabian,

Do you have any example projects with similar workflows (e.g. defining new Scala.Fun functions, writing custom s/h commands etc.)? I have gone through the system manual chapter 5 and it's a bit difficult to see how such a tool is made without an example.

Thanks a lot,
Chengsong

Fabian Huch (May 03 2024 at 07:43):

The Isabelle codebase is the best place to look for examples. For the scala part, I would recommend using an IDE to find the implementors of the abstract Scala.Fun class in src/Pure/System/scala.scala (use isabelle scala_project to generate a version of the sources that an IDE can understand); a few examples are already in the Scala module itself.

As for Isabelle/ML, there is the excellent Isabelle/ML Cookbook as a general resource, and for the s/h command I would simply copy from the existing sledgehammer command and adapt.

Fabian Huch (May 03 2024 at 07:46):

All of this involves a fair bit of work and getting used to the Isabelle code-base, though.

Chengsong Tan (May 03 2024 at 14:03):

Fabian Huch said:

The Isabelle codebase is the best place to look for examples. For the scala part, I would recommend using an IDE to find the implementors of the abstract Scala.Fun class in src/Pure/System/scala.scala (use isabelle scala_project to generate a version of the sources that an IDE can understand); a few examples are already in the Scala module itself.

As for Isabelle/ML, there is the excellent Isabelle/ML Cookbook as a general resource, and for the s/h command I would simply copy from the existing sledgehammer command and adapt.

So how do I generate a "hello world" project that can invoke in some theory context s/h using some Scala code? I have run the command isabelle scala_project in a different folder than src/Pure/System/scala.scala. I assume that has created a project template. But how to fill in the hello world bits in that project? Once I fill in, what tool do I run to compile and execute it, maybe sbt?

Fabian Huch (May 03 2024 at 14:55):

Have a look into the system manual, especially Chapter 5.2 and 5.4 (an example module is also provided in the distribution). There is a hello world example of how to call your Scala function from within ML.

The scala_project tool merely creates a copy of your Isabelle sources. I would recommend running it with the 'symlink' option so changes get reflected back into the actual sources (see the description of that tool, either in the manual or with isabelle scala_project -?.

Generally, the workflow is that you change your sources and run Isabelle. The tool to run compile and execute it is Isabelle. When you change sources and start Isabelle, it does all of that.

Last updated: Dec 21 2024 at 12:33 UTC