[isabelle] Improvement suggestion for isabelle process



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)
    }




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.