[isabelle-dev] NEWS: process management (summary and update)

Lars Noschinski noschinl at in.tum.de
Sun Mar 20 06:41:52 CET 2016


On 11.03.2016 18:37, Makarius wrote:
> * The executable "isabelle_process" has been discontinued. Tools and
> prover front-ends should use ML_Process or Isabelle_Process in
> Isabelle/Scala. INCOMPATIBILITY.
> 
> * New command-line tool "isabelle process" supports ML evaluation of
> literal expressions (option -e) or files (option -f) in the context of a
> given heap image. Errors lead to premature exit of the ML process with
> return code 1.

To whomever is now maintaining Haskabelle (Ondřej?): This change breaks
Haskabelle as it calls isabelle_process to build its adaptation table
(in lib/mk_adapt).

  -- Lars



More information about the isabelle-dev mailing list