Stream: General

Topic: Calling Isabelle incrementally on command line

Chengsong Tan (Sep 04 2023 at 19:36):

Hi all,

Suppose I have a .thy file F and would like to interact with Isabelle via the command line. I want to send Isabelle a small snippet P, say a lemma, a definition or a function.
Is there a way to set F as the "context" and ask Isabelle to give the output it normally gives when you type P in jedit?
This way you can use Isabelle without the limitation of typing speed and try out many examples via some parameterised script.

A simple-minded minimal example:
Let's say F is called CommandLineIsabelle.thy:

theory CommandLineIsabelle imports Main
begin

datatype Counter = C int

inductive
  nextC:: "Counter ⇒ Counter ⇒ bool" ("_ ↝ _" [100, 100] 100)
where
  inc[intro, simp]:"C n ↝ C (n + 1)"
| dec[intro, simp]: "C n ↝ C (n - 1)"

lemma c_goes_to_everywhere: "(rtranclp nextC) (C n)  (C m)"

  oops


end

and P is the snippet

lemma c_goes_to_everywhere: "(rtranclp nextC) (C 0)  (C 9)"
  sledgehammer
  oops

Is there something like a command line isabelle F P
such that the output would be the same as if the output pane of jedit
if you insert P into F just before the end keyword, like this?

theory CommandLineIsabelle imports Main
begin

datatype Counter = C int

inductive
  nextC:: "Counter ⇒ Counter ⇒ bool" ("_ ↝ _" [100, 100] 100)
where
  inc[intro, simp]:"C n ↝ C (n + 1)"
| dec[intro, simp]: "C n ↝ C (n - 1)"

lemma c_goes_to_everywhere: "(rtranclp nextC) (C n)  (C m)"

  oops

lemma c_goes_to_everywhere: "(rtranclp nextC) (C 0)  (C 9)"
  sledgehammer
  oops
(*cursor position *)

end

This way, Isabelle can be used as a testing oracle for an in-development formalisation.

Thanks a lot!

Mathias Fleury (Sep 04 2023 at 20:19):

As far as I know there is a single project using the isabelle server: https://www.tu.berlin/mtv/forschung/projekte/beweisassistenten-in-der-lehre

Mathias Fleury (Sep 04 2023 at 20:19):

and they relied on help from makarius to get that done

Mathias Fleury (Sep 04 2023 at 20:21):

There could also be an alternative relying on the LSP protocol; that could allow for the same thing (but providing less control)

Mathias Fleury (Sep 04 2023 at 20:21):

But in short: no, nothing exist

Mathias Fleury (Sep 04 2023 at 20:21):

and Isabelle/jEdit remains the official way to interact with Isabelle

Chengsong Tan (Sep 05 2023 at 11:48):

Mathias Fleury said:

As far as I know there is a single project using the isabelle server: https://www.tu.berlin/mtv/forschung/projekte/beweisassistenten-in-der-lehre

Thanks Mathias!
I was wondering if you can use command line at all to ask Isabelle to interpret things and give answers.
Something like calling isabelle and ask it to check a .thy file(i.e. needs not be incremental).
I know that you can generate PDFs automatically invoking isabelle command line, but not sure about other usages.

Mathias Fleury (Sep 05 2023 at 11:49):

with a session (the ROOT file) and isabelle build MySessionName

Wenda Li (Sep 05 2023 at 13:28):

Dominique's scala-isabelle could be relevant here, though it is not official by Makarius standard :-)

Andrea Vezzosi (Sep 08 2023 at 11:36):

I have similar needs and I have been trying to look at scala-isabelle for it but it doesn't seem to provide a interface to build a theory/session and get structured feedback about how that went. It provides types for the various components but not specific methods, is the case that you need to know what Isabelle/ML functions to call to do something like that?

Last updated: May 01 2024 at 20:18 UTC