Re: [isabelle] Isabelle2016-RC5 available



On 16 Feb 2016, at 21:42, Makarius <makarius at sketis.net> wrote:
>
> On Tue, 16 Feb 2016, Gerwin Klein wrote:
>
>>> On 13.02.2016, at 05:36, Makarius <makarius at sketis.net> wrote:
>> [..]
>>> Isabelle2016-RC5 is now available for regular use in anticipation of official Isabelle2016:[
>> [..]
>>>  - Poly/ML: hardwired bash in OS.Process.system to help
>>>    Debian-testing-unstable with exported shell functions
>>
>> Just wanted to confirm that this has avoided the problem in our setup as well.
>
> Can you say where the bad dash-0.5.8 in your setup is coming from? So far my impression it that only Debian-testing uses that.

The main (surprising) case happened to be a manual dash update on Ubuntu. Not something youâd currently encounter by default, but potentially an issue in the next few Ubuntu releases.


>> We had some additional dash breakage in Makefiles that were using "isabelle envâ, and the same change of âSHELL=bashâ works there as well.
>
> The "make" tool is indeed another canonical source for /bin/sh invocations. Even though "make" is obsolete for Isabelle, the concept of the Isabelle process environment should allow going through /bin/sh, and just avoiding that is no proper solution in the long term.
>
> I have already plenty of ideas to make it once again more robust -- like I've done several times in the past 1-2 decades. Nonetheless, it is sad that Unix or POSIX has become such a fragile and hostile programming environment. Windows is easier to tame in that respect, because we simply ship a single well-defined version of Cygwin for the POSIX glue.

Indeed.

Cheers,
Gerwin

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.


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