[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