Re: [isabelle] Using ISABELLE_BUILD_OPTIONS in Isabelle 2013



On Thu, 31 Jan 2013, Matthew Fernandez wrote:

Section 3.3 of the Isabelle System Manual [0] indicates that you can use
the environment variable ISABELLE_BUILD_OPTIONS to pass extra -o
arguments to `isabelle build`. I can't get this to work and passing -v
to `isabelle build` confirms that ISABELLE_BUILD_OPTIONS is blank.
Furthermore I get the following behaviour:

On Isabelle 2012:
$ ISABELLE_BUILD_OPTIONS=foo isabelle getenv ISABELLE_BUILD_OPTIONS
ISABELLE_BUILD_OPTIONS=foo

On Isabelle 2013:
$ ISABELLE_BUILD_OPTIONS=foo isabelle getenv ISABELLE_BUILD_OPTIONS
ISABELLE_BUILD_OPTIONS=

It looks to me as if Isabelle 2013 is cleaning this variable. Am I doing
something wrong? How is ISABELLE_BUILD_OPTIONS supposed to be used?

It was already pointed out that Isabelle settings are usually statically scoped, and defined within the Isabelle environment, not outside it via raw "env". (The latter works in exceptional situations only.)


The command-line option -v (verbose) of the "isabelle build" tool is not an ISABELLE_BUILD_OPTION in that sense. The predecessor tool usedir did know the first-class notion of "system options" of Isabelle2013 yet, so it merely imitated that by allowing all command-line options to be made persistent in a slightly odd way.

The general approach of the new isabelle build tool is to have system options to configure it the background (see also "isabelle option" to inspect these), and command-line options to control it in the forground; the command-line option -o allows to modify system options on the spot.

You normally control isabelle build by "letter soup" as for Unix tar, for example. So its command-line options are more like actions. See the examples in the system manual.


Also note that the "isabelle build_dialog" that is built into "isabelle jedit" already provides a simplified build interface that is sufficient in many situations. Another notably short-cut is "isabelle mkroot" to produce a ROOT setup with certain build options.

None of this will allow you to hardwire verbose mode though. You make your own isabelle tool script doing that, or just practice certain build letter-soup habits.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.