[isabelle-dev] isabelle build

Tobias Nipkow nipkow at in.tum.de
Mon Aug 6 12:18:57 CEST 2012


I hope you don't want to abolish "isabelle make" yet, because there will be many
directories out there that require it.

This reminds me: how to turn
Printer.show_question_marks_default := false;
into Isar?

Thanks
Tobias

Am 06/08/2012 12:09, schrieb Makarius:
> Did everybody try the isabelle build tool?  Are there any problems left, apart
> from retraining fingers after 16 years of usedir/make/makeall?
> 
> Isatest and mira already work with the new setup, and AFP is easily fooled via
> some rudimentary HOL/IsaMakefile that contains targets for the images that it
> needs (using isabelle build under the hood).
> 
> This means we are basically ready to dispose the old IsaMakefile + ROOT.ML
> collection.
> 
> 
>     Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev



More information about the isabelle-dev mailing list