Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Improvement suggestion for isabelle process


view this post on Zulip Email Gateway (Oct 10 2020 at 09:03):

From: "Devant, Pascal" <pascal.devant@rwth-aachen.de>
Lately I have been working on a script that automatically runs sledgehammer on unproven lemmas in a given theory. The subcommand 'isabelle process' seemed to be sufficient for this purpose. And this is true if the only goal is to find proofs. However, when it comes to evaluating search times you quickly run into a problem with this approach because 'isabelle process' only returns the output of the underlaying poly process after its' termination.

This "output-after-termination" behaviour has two unpleasant effects:

  1. There is no way to measure the actual search time of specific provers.
  2. A prover might find a proof fairly quick (e.g. after a few seconds) but the user will only get to see the proof ones all other provers have terminated. Since for most non-trivial lemmas there is almost always a prover that will run into a timeout. Hence the whole process is blocked for the set sledgehammer timeout.

After some code inspection, I backtracked the described behaviour to the scala definition of 'result' in "Pure/System/bash.scala". In this definition Isabelle is waiting synchronously for the termination of the poly process by waiting for the result of "File.read_lines".

To "solve" this behaviour I extended the given "Process" class in bash.scala by a modifed version of the existing "result()" method that reads the output stream of poly line by line and immediately redirects it to the console. After creating this method all that was left to do is using this method instead of "result()" in "ml_process.scala"
My modifed version of the result method it attached below. It's most likly not a clean implementation since this is my first scala code but it works. (And this is what matters, I guess)

Is there a special resason why this whole procedure is not made async in the current implementation of Isabelle?
Is there a chance that isabelle process will redirect the output of poly async in future versions of Isabelle, so I don't need to use my own "patched" version?

Thanks for reading!

Best regards,
Pascal

def logAsyncAndWaitForExit(
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
progress_limit: Option[Long] = None,
strict: Boolean = true): Process_Result =
{
stdin.close

var out_lines = new ListBuffer[String]()
Future.thread("async_stdout") {
while(true)
{
val line = stdout.readLine()
if (line != null)
{
Console.println(line)

this.synchronized {
out_lines += line
}
}
}
}

var err_lines = new ListBuffer[String]()
Future.thread("async_stderr") {
while(true)
{
val line = stdout.readLine()
if (line != null)
{
Console.println(line)

this.synchronized {
err_lines += line
}
}
}
}

val rc =
try { join }
catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()

Process_Result(rc, out_lines.toList, err_lines.toList, false, get_timing)
}

view this post on Zulip Email Gateway (Nov 07 2020 at 16:31):

From: Makarius <makarius@sketis.net>
On 10/10/2020 00:43, Devant, Pascal wrote:

Lately I have been working on a script that automatically runs sledgehammer on unproven lemmas in a given theory. The subcommand 'isabelle process' seemed to be sufficient for this purpose. And this is true if the only goal is to find proofs. However, when it comes to evaluating search times you quickly run into a problem with this approach because 'isabelle process' only returns the output of the underlaying poly process after its' termination.

This "output-after-termination" behaviour has two unpleasant effects:
1. There is no way to measure the actual search time of specific provers.
2. A prover might find a proof fairly quick (e.g. after a few seconds) but the user will only get to see the proof ones all other provers have terminated. Since for most non-trivial lemmas there is almost always a prover that will run into a timeout. Hence the whole process is blocked for the set sledgehammer timeout.

This old thread is still open, but it is about potential refinements for the
next release, so an answer now is still on time.

After some code inspection, I backtracked the described behaviour to the scala definition of 'result' in "Pure/System/bash.scala". In this definition Isabelle is waiting synchronously for the termination of the poly process by waiting for the result of "File.read_lines".

I was at first confused by the proposed changes to Process.result, because the
existing operation already supports incremental output via
progress_stdout/progress_stderr.

So here is my minor change to "isabelle process" for incremental output on
stdout/stderr (separately): https://isabelle-dev.sketis.net/rISABELLE6345cce0e576

Is there a special resason why this whole procedure is not made async in the current implementation of Isabelle?

Historically, we used to have sophisticated interaction between the prover
process and Proof General / Emacs: it worked to some extent, but was more
delicate and fragile than one would hope for.

So with the emergence of Isabelle/PIDE process management and interaction
independently of stdin/stdout/stderr, I downgraded old-fashioned processes to
become atomic functions (non-interactive). Only gradually, I added things like
progress_stdout later on.

Depending what you are actually trying to do, the above incremental
stdout/stderr stream might be OK for the purpose.

More ambitious applications could work better with "isabelle server" and and
its explicit JSON message protocol: but that is some extra complexity. You
could also try to implement your tool directly in Isabelle/Scala and use the
underlying Headless.Session directly, without the extra JSON non-sense.

There is quite some documentation on the server in the "system" manual,
chapter 4. For its Headless.Session, the "isabelle dump" tool may serve as
canonical example.

Note that you can browse Isabelle/Scala sources easily with IntelliJ IDEA,
using the project generated by "isabelle scala_project" (see "system" manual
section 5.5).

Makarius


Last updated: Dec 08 2021 at 10:22 UTC