[isabelle] Isabelleâs getsettings somehow broken



Hi,

this is still 2015 (sorry for not helping with beta-testing the next
release at the moment).

I suddenly see this failure building a session with document:

/tmp $ isabelle mkroot -d test
/tmp $ cd test/
/tmp/test $ vim ROOTÂ
# add only one theory, Foo
/tmp/test $ echo 'theory Foo imports Main begin end' > Foo.thy
/tmp/test $ isabelle build -D .
Running test ...

test FAILED
(see also /home/jojo/.isabelle/Isabelle2015/heaps/polyml-5.5.2_x86-linux/log/test)

val it = (): unit
Loading theory "Foo"
### theory "Foo"
### 0.070s elapsed time, 0.140s cpu time, 0.000s GC time
"$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"
Unfinished session(s): test
0:00:10 elapsed time, 0:00:16 cpu time, factor 1.60


Here is what I found so far:

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.

Has anyone else seen this before?


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.