Re: [isabelle] Isabelleâs getsettings somehow broken



Hi,

Am Mittwoch, den 10.02.2016, 15:39 +0100 schrieb Makarius:
> > "$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.

Luckily we have poor souls running sliding update distributions (Debian
unstable here) who can suffer from the fallout in time for it to be
fixed before the other users are affected.

Anyways, the problem also happens with 2016-rc4, so this is likely
something worth investigating before the release. After further
digging, it turns out that it works if /bin/sh does point to /bin/bash
instead of /bin/dash. Bisecting the version ranges of dash, the problem
started to appear in 0.5.8. Likely contender:
http://git.kernel.org/cgit/utils/dash/dash.git/commit/?id=46d3c1a614f11f0d40a7e73376359618ff07abcd

I notified the dash developers about the problem, but dash 0.5.8 will
eventually be used in plenty of places where we probably want to use
Isabelle out of the box, so I suggest to either ensure that bash
scripts within Isabelle call each other via bash only, or (likely more
reliable) do not rely on exporting bash functions via the environment,
but source their definition in every shell.

Greetings,
Joachim


-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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