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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
