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


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