Email Gateway (Aug 19 2022 at 09:50): Email Gateway (Aug 19 2022 at 09:50):From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
Hi all,
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?
Thanks,
Matthew
[0] docs/system.pdf
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 19 2022 at 09:50):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Hi Matt,
you usually set these variables in ~/.isabelle/etc/settings. This gets loaded after the default etc/settings which probably sets the build options to empty.
Cheers,
Gerwin
Email Gateway (Aug 19 2022 at 10:04):From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
On 01/02/13 22:58, Makarius wrote:
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 toisabelle build. I can't get this to work and passing -v
toisabelle buildconfirms 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=fooOn 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.)
Thanks, Makarius. After talking with Gerwin out-of-band I think I've
clarified my own thinking about this. My confusion stemmed from the fact
that you can use isabelle getenv with other environment variables. I
was expecting to have ISABELLE_BUILD_OPTIONS in my shell environment
override that in my settings file.
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.
I think I was a bit unclear here. I was not expecting to be able to
provide -v via ISABELLE_BUILD_OPTIONS. I was merely using -v to get the
output of what ISABELLE_BUILD_OPTIONS was set to. My use case was trying
to provide "document=pdf" via this variable. From what I've gathered,
the only ways to do this are with -o, via my settings file or in the
session definition in ROOT.
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
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 19 2022 at 10:12):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 25 2024 at 12:23 UTC