Re: [isabelle] Isabelleʼs getsettings somehow broken
On Wed, 10 Feb 2016, Joachim Breitner wrote:
this is still 2015 (sorry for not helping with beta-testing the next
release at the moment).
Isabelle2016-RC0 from 01-Jan-2016 could have been called a beta version,
but starting with Isabelle2016-RC1 we are de-facto on the next release.
What remains is a window of oppurtunity to improve it further before it
finalized and becomes unchangable. The window of opportunity closes next
week, as far as I can foresee now.
"$ISABELLE_TOOL" document -o 'pdf' -n 'document' -t '' 'output/document' 2>&1
*** /opt/isabelle/Isabelle2015/bin/isabelle: Zeile 52: splitarray: Kommando nicht gefunden.
*** Unknown Isabelle tool: document
*** Failed to build document "/tmp/test/output/document.pdf"
splitarray is a bash function defined in lib/scripts/getsettings, which
exports a bunch of variables and functions to the environment, (using
"set -o allexport"). It also exports ISABELLE_SETTINGS_PRESENT and does
nothing if it finds that variable to be set.
It seems that when isabelle build calls isabelle document, it somehow
has ISABELLE_SETTINGS_PRESENT in the environment (thus making the line
source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
in bin/isabelle do nothing), but not the bash function splitarray (thus
making the program fail).
It must be a recent change in my system, but my bash package has not
changed since September, and I canʼt imagine what other package might
have caused this.
The Isabelle process environment is indeed built up only once, and then
passed to subprocesses according to normal Unix discipline.
Since splitarray is a shell function, not just a simple environment
variable, it can get lost when alien shells are invoked in the process
hierarchy. It should usually work with Bourne-shell variants and some
other well-known shells, but have seen it fail many years ago with
versions of /bin/sh that don't know what they really are.
Such details can change spontaneously on various Linux distributions,
especially those that have very dynamic or "sliding" updates: somebody
"fixes" a shell, and afterwards many things are broken.
This archive was generated by a fusion of
Pipermail (Mailman edition) and