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 
bad /bin/sh.

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 /bin/bash.

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.


	Makarius


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