Re: [isabelle] Isabelleʼs getsettings somehow broken
On Wed, 10 Feb 2016, Joachim Breitner wrote:
So patching Poly/ML could work, but anybody doing plain Unix programming
with "system" functions (e.g. in perl) will fall again on his nose with a
Only (in the context of the current issue) if this system programming
happens in a process called by isabelle and itself calls isabelle again.
Is that something we should worry about?
I did worry about it when consolidating the current setup in the past few
years. There is a long history behind all this, trying to dodge problems
on various DOS or Unix variants -- many of them no longer exist. The shell
functions solve certain problems from the past.
The key principle is that the Isabelle process environment is preserved
faithfully, through process trees, no matter how they are built up via
normal Unix programming: this involves occasionally /bin/sh invocations by
programs and libraries that are not under our control.
Have you considered, as a middle way, to keep the
ISABELLE_SETTINGS_PRESENT-logic in lib/scripts/getsettings that
determines the settings once, but within this if..then..else block only
set genuine environment variables, and after the else block, define all
the bash functions unexported.
I did, some hours ago, and rejected it. It would mean to introduce
workarounds in order to avoid casualties in a war between /bin/dash and
Presently, I would rather invest time to raise attention to the dash
problem on various trackers. It seems that apart from Ubuntu and Debian,
hardly anybody else is infected by the "dash is the better /bin/sh" idea.
This archive was generated by a fusion of
Pipermail (Mailman edition) and