[isabelle-dev] isabelle build

[Makarius]

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