Re: [isabelle] Isabelleʼs getsettings somehow broken
On Wed, 10 Feb 2016, Joachim Breitner wrote:
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:
That change is from 2012. My impression is that the bash guys have already
taken measures against such "sanitised environments" some years ago: the
shell functions are represented as regular assignments of the form A=B,
e.g. BASH_FUNC_isabelle_scala%%=() ...
I notified the dash developers about the problem, but dash 0.5.8
There must be a new problem in dash 0.5.8. I have Unbuntu 15.10 with dash
0.5.7 and can do the following:
$ isabelle env dash
$ type isabelle
isabelle is a function
If it is not a function, it got somehow mangled.
It is also possible to inspect the full "env" with that command.
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
I've spent some years on variations on all that already, refining it over
and over again.
Isabelle exclusively uses bash wherever possible. Sometimes other system
function sneak-in unreliable /bin/sh.
What is your $SHELL actually?
Everytime such incidents happen, I consider giving up Linux (although I am
running it myself).
This archive was generated by a fusion of
Pipermail (Mailman edition) and