Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Premise extraction with the use of Isabelle/Scala


view this post on Zulip Email Gateway (Jun 07 2022 at 13:55):

From: Makarius <makarius@sketis.net>
The thm_deps command is indeed of relatively little practical relevance: It
inspects the internal derivation, i.e. the low-level implementation of a
proof. This can contain almost arbitrary "rubbish".

Makarius

view this post on Zulip Email Gateway (Jun 07 2022 at 13:56):

From: Makarius <makarius@sketis.net>
Abstractly, it sounds like you should start within Isabelle/ML, but some
interaction with Isabelle/Scala will be required (e.g. to "see" which facts
were used in the text).

An alternative is to start in Isabelle/Scala (with PIDE context), and interact
with Isabelle/ML via so-called "print functions". E.g. see examples in
Pure/PIDE/query_operation.ML (and .scala).

When you say "visible facts in the current context", what does it mean?

* The proof state (with its formal Proof.context in Isabelle/ML)?

* The surrounding Isar proof text, leading to a goal?

* Something else?

Makarius

view this post on Zulip Email Gateway (Jun 07 2022 at 13:56):

From: Makarius <makarius@sketis.net>
The task is certainly difficult, but there are two areas of difficulties that
should be clearly separated:

(1) Conceptual: What are you trying to do? What is the context? What do you
want to achieve?

(2) Technical: Can this be done just with standard Isabelle/ML +
Isabelle/Scala operations? What is the purpose of non-standard python and
scala-isabelle?

Makarius

view this post on Zulip Email Gateway (Jun 07 2022 at 13:59):

From: Makarius <makarius@sketis.net>
It seems that you did not answer this back to the mailing list. Thus is will
cause a lot of confusion about "who said what" in the ongoing discussion.

Makarius

view this post on Zulip Email Gateway (Jun 08 2022 at 21:16):

From: Szymon Antoniak <sa394197@students.mimuw.edu.pl>
In effort to straighten the email history, I will respond here and hopefully establish some linearity from this point on.
As to the visible facts, what I mean by that is all the possible theorems/lemmas that sledgehammer gets to see before applying the relevance filter (i.e. what could appear at the position of the dots in by (metis ...)).

Szymon

7 czerwca 2022 15:55, "Makarius" <makarius@sketis.net> napisał/-a/:

view this post on Zulip Email Gateway (Jun 18 2022 at 09:11):

From: Makarius <makarius@sketis.net>

On 07/06/2022 15:21, Szymon Antoniak wrote:

High-level, we want to be a better premise selector than, say, MePo (or
MePo + Sledgehammer, just
as well). What we want to do is to take all the visible facts in the
current context and select
relevant ones. For that, we have to have a dataset to train our selection
model on, and that
dataset requires that for each step, we specify what facts were used in
that step.
The python part is really just redundant information (we use this to
interact with the environment,
but for this extraction it is absolutely not needed and Isabelle/Scala
suffices), we can only
restrict ourselves to Isabelle/ML and Isabelle/Scala.

Abstractly, it sounds like you should start within Isabelle/ML, but some
interaction with
Isabelle/Scala will be required (e.g. to "see" which facts were used in
the text).

An alternative is to start in Isabelle/Scala (with PIDE context), and
interact with Isabelle/ML via
so-called "print functions". E.g. see examples in
Pure/PIDE/query_operation.ML (and .scala).

When you say "visible facts in the current context", what does it mean?

(Cleaning up old threads, I've found this one still half-open.)

Reading it again, I would say you should look in Isabelle/ML how sledgehammer
manages its facts. You can browse the thy/ML sources of Isabelle/HOL, by
starting the Prover IDE with Isabelle/Pure and open the sources (first some
theory, then some corresponding ML files).

For example in the main directory of Isabelle2021-1:

isabelle jedit -l Pure src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML

I can take quite some time until everything required for this context is
checked in the Prover IDE. Afterwards you can jump around in the files via
formal links etc.

It could also make sense to open src/HOL/Main.thy e.g. if you need other ML
files with richer theory context.

Makarius


Last updated: Jul 15 2022 at 23:21 UTC