Re: [isabelle] Isabelle2016-RC5 available



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.


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.


	Makarius


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