[isabelle-dev] Data slots for runtime compiler invocation

Makarius makarius at sketis.net
Mon Jan 10 18:15:37 CET 2011


On Mon, 10 Jan 2011, Florian Haftmann wrote:

> Recently I changed the interface for invoking the compiler at runtime on 
> generated code to use proof data slots rather than unsychronized 
> references.  The consequence is that there are a lot of non-joinable 
> proof data slots laying around in the same module, cf. 
> http://isabelle.in.tum.de/reports/Isabelle/rev/f6ab14e61604

Which are the non-joinable ones in particular? Did I overlook anything 
important?


 	Makarius



More information about the isabelle-dev mailing list