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

Makarius makarius at sketis.net
Tue May 24 20:15:27 CEST 2016


On 20/03/16 06:41, Lars Noschinski wrote:
> 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).

This seems to be still open.

Is there a remaining maintainer of Haskabelle?


	Makarius




More information about the isabelle-dev mailing list