[isabelle-dev] isabelle build
makarius at sketis.net
Mon Aug 6 13:48:24 CEST 2012
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
The existing ROOT files in the Isabelle sources represent examples how to
deal with this and other (more complex) cases.
More information about the isabelle-dev