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: http://git.kernel.org/cgit/utils/dash/dash.git/commit/?id=46d3c1a614f11f0d40a7e73376359618ff07abcd

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
$ bash
$ type isabelle
isabelle is a function
isabelle ()
{
    "$ISABELLE_TOOL" "$@"
}

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 shell.

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).


	Makarius




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