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.


	Makarius


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