Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Example Projects manipulating Isabelle/Scala, ...

view this post on Zulip Email Gateway (May 03 2024 at 14:58):

From: "Tan, Chengsong" <c.tan@imperial.ac.uk>
Hi all,

Are there any existing projects that uses Isabelle/Scala and Isabelle/ML to define custom Scala.Fun functions and also develop custom sledgehammer commands invoking these functions? I want to build an automated tool that copy-pastes sledgehammer proofs for you (details in https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/tools.20to.20automatically.20adopt.20sledgehammer.20proofs.20into.20theory),
and I have been looking at the system manual (chapter 5), but without an example it is difficult to set up a "hello world" prototype to start with.

Thanks a lot!

Best wishes,
Chengsong

view this post on Zulip Email Gateway (May 04 2024 at 11:08):

From: Makarius <makarius@sketis.net>
In Isabelle2024-RC3 there is src/Tools/Demo to show how to make a command-line
tool in Isabelle/Scala: that directory is registered implicitly as
"component". For your own setup, you need to do this explicitly, e.g. via
"isabelle components -u".

To register Scala functions instead of command-line tools, the relevant
service class is Scala.Functions. If you hyper-search that in all .scala
sources, you will see examples. You need to make your own instance and
register that in etc/build.props in the section "services".

Makarius

view this post on Zulip Email Gateway (May 06 2024 at 11:37):

From: "Tan, Chengsong" <c.tan@imperial.ac.uk>
Hi Makarius,

Thanks a lot for the Demo info, I have now created and registered my own command-line tool.
How to I call sledgehammer from Isabelle/Scala (or Isabelle ML)? Like, is there some API that allows me to call sledgehammer from a method in “demo_tool.scala”? Can I do something like: "Here's this thy file. Tell me what's the sledgehammer output at line 100 column 45"?
I can see that there are functions like “run_atp” and “one_line_proof_text” in the relevant .ML files in the “HOL/Tools/Sledgehammer” folder, but am not quite sure how to leverage them to achieve the above effect.

Thanks a lot,
Chengsong

Last updated: May 19 2024 at 04:18 UTC