isabelle: Admin/polyml/README@a2351f82bc48 (annotated)

38469 5c6c5d63f3c3 updated for prospective Poly/ML 5.4; wenzelm parents: 37122 diff changeset	1	Poly/ML for Isabelle
5c6c5d63f3c3 updated for prospective Poly/ML 5.4; wenzelm parents: 37122 diff changeset	2	====================
27012 e6229d8d6aaa moved README-polyml to polyml/README; wenzelm parents: diff changeset	3
62252 6a87f7b15b69 updated to official polyml-5.6; wenzelm parents: 62199 diff changeset	4	This compilation of Poly/ML 5.6 (http://www.polyml.org) is based on the source
6a87f7b15b69 updated to official polyml-5.6; wenzelm parents: 62199 diff changeset	5	distribution from https://github.com/polyml/polyml/releases/tag/v5.6/.
57689 e189ba8a64b9 updated to polyml-5.5.2-1 which addresses two hard crashes; wenzelm parents: 56958 diff changeset	6
62281 707f9b182f4f evade a potential conflict of /bin/bash versus /bin/sh -> dash (notably on Ubuntu and Debian) -- note that execvpe does not exist on old glibc on Ubuntu 10.04 LTS, but the environ should be unchanged; wenzelm parents: 62252 diff changeset	7	On Linux the sources have changed as follows, in order to evade a
707f9b182f4f evade a potential conflict of /bin/bash versus /bin/sh -> dash (notably on Ubuntu and Debian) -- note that execvpe does not exist on old glibc on Ubuntu 10.04 LTS, but the environ should be unchanged; wenzelm parents: 62252 diff changeset	8	potential conflict of /bin/bash versus /bin/sh -> dash (notably on
707f9b182f4f evade a potential conflict of /bin/bash versus /bin/sh -> dash (notably on Ubuntu and Debian) -- note that execvpe does not exist on old glibc on Ubuntu 10.04 LTS, but the environ should be unchanged; wenzelm parents: 62252 diff changeset	9	Ubuntu and Debian):
707f9b182f4f evade a potential conflict of /bin/bash versus /bin/sh -> dash (notably on Ubuntu and Debian) -- note that execvpe does not exist on old glibc on Ubuntu 10.04 LTS, but the environ should be unchanged; wenzelm parents: 62252 diff changeset	10
707f9b182f4f evade a potential conflict of /bin/bash versus /bin/sh -> dash (notably on Ubuntu and Debian) -- note that execvpe does not exist on old glibc on Ubuntu 10.04 LTS, but the environ should be unchanged; wenzelm parents: 62252 diff changeset	11	diff -r src-orig/libpolyml/process_env.cpp src/libpolyml/process_env.cpp
707f9b182f4f evade a potential conflict of /bin/bash versus /bin/sh -> dash (notably on Ubuntu and Debian) -- note that execvpe does not exist on old glibc on Ubuntu 10.04 LTS, but the environ should be unchanged; wenzelm parents: 62252 diff changeset	12	228c228
707f9b182f4f evade a potential conflict of /bin/bash versus /bin/sh -> dash (notably on Ubuntu and Debian) -- note that execvpe does not exist on old glibc on Ubuntu 10.04 LTS, but the environ should be unchanged; wenzelm parents: 62252 diff changeset	13	< execve("/bin/sh", argv, environ);
707f9b182f4f evade a potential conflict of /bin/bash versus /bin/sh -> dash (notably on Ubuntu and Debian) -- note that execvpe does not exist on old glibc on Ubuntu 10.04 LTS, but the environ should be unchanged; wenzelm parents: 62252 diff changeset	14	---
707f9b182f4f evade a potential conflict of /bin/bash versus /bin/sh -> dash (notably on Ubuntu and Debian) -- note that execvpe does not exist on old glibc on Ubuntu 10.04 LTS, but the environ should be unchanged; wenzelm parents: 62252 diff changeset	15	> execvp("bash", argv);
707f9b182f4f evade a potential conflict of /bin/bash versus /bin/sh -> dash (notably on Ubuntu and Debian) -- note that execvpe does not exist on old glibc on Ubuntu 10.04 LTS, but the environ should be unchanged; wenzelm parents: 62252 diff changeset	16
707f9b182f4f evade a potential conflict of /bin/bash versus /bin/sh -> dash (notably on Ubuntu and Debian) -- note that execvpe does not exist on old glibc on Ubuntu 10.04 LTS, but the environ should be unchanged; wenzelm parents: 62252 diff changeset	17
41330 a4d9831c21d4 updated for Poly/ML 5.4.0; wenzelm parents: 38469 diff changeset	18	The included build script is used like this:
a4d9831c21d4 updated for Poly/ML 5.4.0; wenzelm parents: 38469 diff changeset	19
a4d9831c21d4 updated for Poly/ML 5.4.0; wenzelm parents: 38469 diff changeset	20	./build src x86-linux --with-gmp
a4d9831c21d4 updated for Poly/ML 5.4.0; wenzelm parents: 38469 diff changeset	21	./build src x86_64-linux --with-gmp
a4d9831c21d4 updated for Poly/ML 5.4.0; wenzelm parents: 38469 diff changeset	22	./build src x86-darwin --without-gmp
a4d9831c21d4 updated for Poly/ML 5.4.0; wenzelm parents: 38469 diff changeset	23	./build src x86_64-darwin --without-gmp
60983 ff4a67c65084 updated to polyml-5.5.3-20150820, with native x86-windows support; wenzelm parents: 60188 diff changeset	24	./build src x86-windows --with-gmp
61071 c6ac3c3fbb85 support x86_64-windows; wenzelm parents: 60983 diff changeset	25	./build src x86_64-windows --with-gmp
41330 a4d9831c21d4 updated for Poly/ML 5.4.0; wenzelm parents: 38469 diff changeset	26
41331 8cdadd543fc8 tuned; wenzelm parents: 41330 diff changeset	27	Also note that the separate "sha1" library module is required for
62252 6a87f7b15b69 updated to official polyml-5.6; wenzelm parents: 62199 diff changeset	28	efficient digestion of strings according to SHA-1.
41331 8cdadd543fc8 tuned; wenzelm parents: 41330 diff changeset	29
8cdadd543fc8 tuned; wenzelm parents: 41330 diff changeset	30
57689 e189ba8a64b9 updated to polyml-5.5.2-1 which addresses two hard crashes; wenzelm parents: 56958 diff changeset	31	Makarius
62281 707f9b182f4f evade a potential conflict of /bin/bash versus /bin/sh -> dash (notably on Ubuntu and Debian) -- note that execvpe does not exist on old glibc on Ubuntu 10.04 LTS, but the environ should be unchanged; wenzelm parents: 62252 diff changeset	32	11-Feb-2016

author	wenzelm
	Wed, 16 Mar 2016 22:19:08 +0100
changeset 62645	a2351f82bc48
parent 62281	707f9b182f4f
child 64544	d23b7c9b9dd4
permissions	-rw-r--r--