Email Gateway (May 03 2024 at 14:58): 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
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
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
Email Gateway (Jun 02 2024 at 09:51):From: "Tan, Chengsong" <c.tan@imperial.ac.uk>
The offset counts Isabelle symbols from the start of the identified text. One
approach to get line (and column) from it is to turn it into a Text.Offset and
then use Line.Node_Position.advance with the substring in question. If you
search the Isabelle/Scala sources for Line.Node_Position, you will see some
examples.
How is such id and offset in ML converted to Scala?
The hope is that such id and offset information can be used to calculate the text (line & col) position a certain command, when that command is being evaluated in ML, which usually means that information is no longer available.
ML and Scala interface via some protocol, therefore whenever a command generates some output/causes a state change in ML, then that information must be passed back to Scala via the protocol message. My idea is that we can intercept that message (which will contain necessary info to deduce a Scala offset and id (Symbol.offset and Document_ID.Generic)), so that we can log/render that positional information together with that message. For instance, an ML error causes the jedit proof interface to show several red bits in both the main editor window and the proof state panel, with messages like “Failed to finish proof…”, if we would like to intercept that error message while it is being sent from Isabelle/ML to Isabelle/Scala and add a line number to that message, which files should we modify?
A related question: how are the command_keywords called from the Scala side? These commands are defined in ML, but their calling sites seem not within the ML codebase itself. For instance, sledgehammer’s command keyword is defined with a call to the function “hammer_away”. But who calls hammer_away whenever a sledgehammer is seen in a thy file? Surely in Scala there should be some “handle” that calls hammer_away at sledgehammer?
In a standalone tool like demo_tool.scala, how to convert a thy file (string) into some Isabelle internal representation of proof state? Is that possible?
Thanks a lot,
Chengsong
From: Makarius <makarius@sketis.net>
Date: Monday, 20 May 2024 at 19:37
To: Tan, Chengsong <c.tan@imperial.ac.uk>, isabelle-users@cl.cam.ac.uk <isabelle-users@cl.cam.ac.uk>
Subject: Re: [isabelle] Example Projects manipulating Isabelle/Scala, Isabelle/ML & Sledgehammer
On 12/05/2024 01:32, Tan, Chengsong wrote:
When the line number is not available in Position.T, how to deduce the line
number/character number via “id” and “offset”?
The id is an abstract handle on the piece of text you are looking at. In the
Prover IDE it is the static or dynamic command-span. In batch-mode it is the
overall theory.
The offset counts Isabelle symbols from the start of the identified text. One
approach to get line (and column) from it is to turn it into a Text.Offset and
then use Line.Node_Position.advance with the substring in question. If you
search the Isabelle/Scala sources for Line.Node_Position, you will see some
examples.
I can see that the clickable areas are defined via a function called
“sendback_markup_command” in “active.ML”. So surely with “id” it’s possible to
locate where that command is (so that the text is properly inserted back as
done in s/h for example).
You should look in the vicinity of snapshot.find_command_position and
snapshot.find_command_line to get an idea how this works.
If deducing the specific line from “id” is not possible, is to
“automatically” do the click within Isabelle/ML rather than waiting for user
input. Can you explain a bit more about those clickable “sendback”s so that I
can write such a function?
The sendback markup is produced in Isabelle/ML and interpreted in
Isabelle/Scala in jedit_rendering.scala and active.scala --- the latter uses
build.props "services" of type Active.Handler: that means you could in
principle invent your own markup and provide a specific handler.
This won't help to "do the click in Isabelle/ML", at least not directly. In
fact, the usual approach is abstain from machine generated edits, but merely
offer the user a suitable message with markup to be clicked on.
An example is the document antiquotation for jEdit actions, e.g.
text ‹☛‹about››
A side question, what’s the meaning of all the variables with the suffix “N”,
like sledgehammerN, markup.idN, etc.?
It means "Name".
Makarius
Last updated: Jan 04 2025 at 20:18 UTC