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

author	wenzelm
	Sun, 24 Nov 2019 22:54:42 +0100
changeset 71160	625df1eb7873
parent 71118	2bc568573a47
child 71492	a296d3697e50
permissions	-rw-r--r--