On Mon, 6 Aug 2012, Tobias Nipkow wrote:

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

There will be the usual "legacy" phase of one or two release cycles.
The plan is to keep "isabelle usedir" and "isabelle make" for some time.

Note that "isabelle make" alone does not do anything else than

  make -f IsaMakefile "$@"

within the Isabelle settings environment; without any IsaMakefile it will not do anything.


So users can continue with their own usedir/make setup for some time, but for any of the official images they should use something like

  isabelle build -b HOLCF

potentially within their own legacy make file.


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

This is handled by external Isabelle options, see etc/options for the main place where they are introduced at the moment. (I still need to unify this new concept with the existing "configuration options" inside the formal context.)

The existing ROOT files in the Isabelle sources represent examples how to deal with this and other (more complex) cases.


        Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to