isabelle: Admin/polyml/README@02e0458d342f (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
69704 3fb94d9b87b0 updated polyml platform: 32=x86_64_32; wenzelm parents: 68702 diff changeset	4	This compilation of Poly/ML (https://www.polyml.org) is based on the
3fb94d9b87b0 updated polyml platform: 32=x86_64_32; wenzelm parents: 68702 diff changeset	5	repository version
69871 02e0458d342f updated to polyml-5.8-20190306; wenzelm parents: 69822 diff changeset	6	https://github.com/polyml/polyml/commit/fef9f8681c2f (master).
57689 e189ba8a64b9 updated to polyml-5.5.2-1 which addresses two hard crashes; wenzelm parents: 56958 diff changeset	7
69704 3fb94d9b87b0 updated polyml platform: 32=x86_64_32; wenzelm parents: 68702 diff changeset	8	The Isabelle repository provides the administrative tool
3fb94d9b87b0 updated polyml platform: 32=x86_64_32; wenzelm parents: 68702 diff changeset	9	"build_polyml", which can be used in the polyml component directory as
3fb94d9b87b0 updated polyml platform: 32=x86_64_32; wenzelm parents: 68702 diff changeset	10	follows.
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	11
64544 d23b7c9b9dd4 updated Poly/ML repository test version (08-Dec-2016); wenzelm parents: 62281 diff changeset	12	* Linux:
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	13
67593 5efb88c90051 clarified command-line defaults; wenzelm parents: 67589 diff changeset	14	$ isabelle build_polyml -m32 -s sha1 src
5efb88c90051 clarified command-line defaults; wenzelm parents: 67589 diff changeset	15	$ isabelle build_polyml -m64 -s sha1 src
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	16
67595 5b4dd7a5b882 tuned; wenzelm parents: 67593 diff changeset	17	* Mac OS X:
5b4dd7a5b882 tuned; wenzelm parents: 67593 diff changeset	18
5b4dd7a5b882 tuned; wenzelm parents: 67593 diff changeset	19	$ isabelle build_polyml -m32 -s sha1 src
5b4dd7a5b882 tuned; wenzelm parents: 67593 diff changeset	20	$ isabelle build_polyml -m64 -s sha1 src
5b4dd7a5b882 tuned; wenzelm parents: 67593 diff changeset	21
64544 d23b7c9b9dd4 updated Poly/ML repository test version (08-Dec-2016); wenzelm parents: 62281 diff changeset	22	* Windows (Cygwin shell)
d23b7c9b9dd4 updated Poly/ML repository test version (08-Dec-2016); wenzelm parents: 62281 diff changeset	23
67593 5efb88c90051 clarified command-line defaults; wenzelm parents: 67589 diff changeset	24	$ isabelle build_polyml -M /cygdrive/c/msys64 -m32 -s sha1 src
5efb88c90051 clarified command-line defaults; wenzelm parents: 67589 diff changeset	25	$ isabelle build_polyml -M /cygdrive/c/msys64 -m64 -s sha1 src
41331 8cdadd543fc8 tuned; wenzelm parents: 41330 diff changeset	26
67589 085f5c2e11f7 support for libgmp for x86-darwin; wenzelm parents: 67583 diff changeset	27
085f5c2e11f7 support for libgmp for x86-darwin; wenzelm parents: 67583 diff changeset	28	Building libgmp on Mac OS X
085f5c2e11f7 support for libgmp for x86-darwin; wenzelm parents: 67583 diff changeset	29	===========================
085f5c2e11f7 support for libgmp for x86-darwin; wenzelm parents: 67583 diff changeset	30
67593 5efb88c90051 clarified command-line defaults; wenzelm parents: 67589 diff changeset	31	The build_polyml invocations above implicitly use the GNU Multiple Precision
5efb88c90051 clarified command-line defaults; wenzelm parents: 67589 diff changeset	32	Arithmetic Library (libgmp), but that is not available on Mac OS X by default.
5efb88c90051 clarified command-line defaults; wenzelm parents: 67589 diff changeset	33	Appending "--without-gmp" to the command-line omits this library. Building
67595 5b4dd7a5b882 tuned; wenzelm parents: 67593 diff changeset	34	libgmp properly from sources works as follows (library headers and binaries
5b4dd7a5b882 tuned; wenzelm parents: 67593 diff changeset	35	will be placed in /usr/local).
67589 085f5c2e11f7 support for libgmp for x86-darwin; wenzelm parents: 67583 diff changeset	36
085f5c2e11f7 support for libgmp for x86-darwin; wenzelm parents: 67583 diff changeset	37	* Download:
085f5c2e11f7 support for libgmp for x86-darwin; wenzelm parents: 67583 diff changeset	38
085f5c2e11f7 support for libgmp for x86-darwin; wenzelm parents: 67583 diff changeset	39	$ curl https://gmplib.org/download/gmp/gmp-6.1.2.tar.xz \| xz -dc \| tar xf -
085f5c2e11f7 support for libgmp for x86-darwin; wenzelm parents: 67583 diff changeset	40	$ cd gmp-6.1.2
67583 c933a5d4e1ee support for libgmp for x86_64-darwin; wenzelm parents: 67099 diff changeset	41
69704 3fb94d9b87b0 updated polyml platform: 32=x86_64_32; wenzelm parents: 68702 diff changeset	42	* build:
67589 085f5c2e11f7 support for libgmp for x86-darwin; wenzelm parents: 67583 diff changeset	43
085f5c2e11f7 support for libgmp for x86-darwin; wenzelm parents: 67583 diff changeset	44	$ make distclean
085f5c2e11f7 support for libgmp for x86-darwin; wenzelm parents: 67583 diff changeset	45	$ ./configure --enable-cxx --build=core2-apple-darwin"$(uname -r)"
085f5c2e11f7 support for libgmp for x86-darwin; wenzelm parents: 67583 diff changeset	46	$ make && make check
085f5c2e11f7 support for libgmp for x86-darwin; wenzelm parents: 67583 diff changeset	47	$ sudo make install
67583 c933a5d4e1ee support for libgmp for x86_64-darwin; wenzelm parents: 67099 diff changeset	48
41331 8cdadd543fc8 tuned; wenzelm parents: 41330 diff changeset	49
57689 e189ba8a64b9 updated to polyml-5.5.2-1 which addresses two hard crashes; wenzelm parents: 56958 diff changeset	50	Makarius
69871 02e0458d342f updated to polyml-5.8-20190306; wenzelm parents: 69822 diff changeset	51	06-Mar-2019

author	wenzelm
	Wed, 06 Mar 2019 19:29:46 +0100
changeset 69871	02e0458d342f
parent 69822	8c587dd44f51
child 69903	63721ee8c86c
permissions	-rw-r--r--