Re: [isabelle] Isabelleâs getsettings somehow broken


> I wonder how such moves from Debian to Ubuntu really work. Are there 
> really imports from Debian-testing into a stable Ubuntu? There are plenty 
> of websites about that, but it also requires time to study them. 
> has DebianImportFreeze 
> for 17-Feb-2016 -- whatever that means.

well spotted, thanks. It means
    Prior to this date, new versions of packages will be automatically
    imported from Debian where they have not been customized for Ubuntu
    (    )
but dash is customized for Ubuntu, so it will not get merged
automatically. There is still a not too slim chance that it will be
merged manually. So the likelyhood of the next Ubuntu LTS release
shipping dash 0.5.8 is large enough to conservatively assume that to be
the case.

> 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?

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. Some of them are (like spiltarray) are
defined unconditionally and not really settings anyways; only few
functions have definitions that depend on the environmens (namely tar,
jvmpath, isabelle_admin_build). You could define them conditional on
the variables set above. This would give you the desired scoping
behavior for genuine settings, while not relying on treacherous
features such as exporting code between processes.


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

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