[isabelle-dev] Future and maintainance of ~isabelle/contrib_devel at TUM NFS

Makarius makarius at sketis.net
Thu Jul 5 12:00:36 CEST 2012


On Thu, 5 Jul 2012, Florian Haftmann wrote:

> @Gerwin: maybe you could consider adjusting isatest accordingly:
> * use /home/isabelle/contrib instead of /home/isabelle/contrib_devel
> * use Admin/init_components appropriately

I have also started thinking about the full inclusion of 
Admin/init_components into isatest, but my tendency was not to do it for 
now.

In the past we occasionally had a situation where things depending on 
certain non-default or non-free components ended up in the basic 
Isabelle/HOL libraries, and isatest would rightly reject that.


 	Makarius



More information about the isabelle-dev mailing list