Hi,
Thanks for your great work on polyml 5.5. I'd like to bump polyml in Gentoo portage, however this one test fails in the test suite:
./configure --prefix=/usr --build=x86_64-pc-linux-gnu --host=x86_64-pc-linux-gnu --mandir=/usr/share/man --infodir=/usr/share/info --datadir=/usr/share --sysconfdir=/etc --localstatedir=/var/lib --libdir=/usr/lib64 --disable-dependency-tracking --with-x --with-gmp --without-portable --with-threads
...
make tests
...
Test071.ML => Failed!!
...
This is 64 bit amd64 (Intel Core i7) Gentoo linux with gcc 4.7.1, no patches applied to polyml 5.5.
Thanks, Mark
$ emerge --info '=dev-lang/polyml-5.5' Portage 2.1.11.17 (default/linux/amd64/10.0/developer, gcc-4.7.1, glibc-2.15-r2, 3.5.4-gentoo x86_64) ================================================================= System Settings ================================================================= System uname: Linux-3.5.4-gentoo-x86_64-Intel-R-_Core-TM-_i7_CPU_X_940_@_2.13GHz-with-gentoo-2.1 Timestamp of tree: Wed, 19 Sep 2012 04:45:01 +0000 app-shells/bash: 4.2_p37 dev-lang/python: 2.7.3-r2, 3.2.3 dev-util/cmake: 2.8.9 dev-util/pkgconfig: 0.27.1 sys-apps/baselayout: 2.1-r1 sys-apps/openrc: 0.9.8.4 sys-apps/sandbox: 2.5 sys-devel/autoconf: 2.68 sys-devel/automake: 1.10.3, 1.11.6 sys-devel/binutils: 2.22-r1 sys-devel/gcc: 4.5.3-r2, 4.6.3, 4.7.1 sys-devel/gcc-config: 1.7.3 sys-devel/libtool: 2.4-r1 sys-devel/make: 3.82-r3 sys-kernel/linux-headers: 3.5 (virtual/os-headers) sys-libs/glibc: 2.15-r2 Repositories: gentoo lisp gentoo-haskell kde-sunset emacs x-portage ACCEPT_KEYWORDS="amd64" ACCEPT_LICENSE="* -@EULA" CBUILD="x86_64-pc-linux-gnu" CFLAGS="-O2 -march=native -pipe" CHOST="x86_64-pc-linux-gnu" CONFIG_PROTECT="/etc /usr/share/config /usr/share/gnupg/qualified.txt" CONFIG_PROTECT_MASK="/etc/ca-certificates.conf /etc/env.d /etc/fonts/fonts.conf /etc/gconf /etc/gentoo-release /etc/revdep-rebuild /etc/sandbox.d /etc/terminfo /etc/texmf/language.dat.d /etc/texmf/language.def.d /etc/texmf/updmap.d /etc/texmf/web2c" CXXFLAGS="-O2 -march=native -pipe" DISTDIR="/usr/portage/distfiles" EMERGE_DEFAULT_OPTS="-j8 --ask-enter-invalid --autounmask=n" FCFLAGS="-O2 -pipe" FEATURES="assume-digests binpkg-logs collision-protect config-protect-if-modified distlocks ebuild-locks fixlafiles multilib-strict news parallel-fetch protect-owned sandbox sfperms sign splitdebug strict test unknown-features-warn unmerge-logs unmerge-orphans userfetch userpriv usersandbox" FFLAGS="-O2 -pipe" GENTOO_MIRRORS="http://mirror.internode.on.net/pub/gentoo http://ftp.swin.edu.au/gentoo http://ftp.jaist.ac.jp/pub/Linux/Gentoo/" LANG="en_AU.UTF-8" LDFLAGS="-Wl,--hash-style=gnu -Wl,-O1 -Wl,--as-needed" MAKEOPTS="-j8" PKGDIR="/usr/portage/packages" PORTAGE_CONFIGROOT="/" PORTAGE_RSYNC_OPTS="--recursive --links --safe-links --perms --times --compress --force --whole-file --delete --stats --human-readable --timeout=180 --exclude=/distfiles --exclude=/local --exclude=/packages" PORTAGE_TMPDIR="/var/tmp" PORTDIR="/usr/portage" PORTDIR_OVERLAY="/var/lib/layman/lisp /var/lib/layman/haskell /var/lib/layman/kde-sunset /var/lib/layman/emacs /usr/local/portage" SYNC="rsync://rsync.au.gentoo.org/gentoo-portage" USE="X a52 aac acl acpi alsa amd64 berkdb bluetooth branding bzip2 cairo cdda cdparanoia cdr cjk cli consolekit corefonts cracklib crypt cups cxx dbus declarative dri dts dvd dvdr emacs emboss encode examples exif fam ffmpeg firefox flac fortran gcj gd gdbm gdu gif ginac gphoto2 gpm gsm gtk hal hoogle hscolour iconv icu ieee1394 imap ipv6 jpeg kde kipi lcms ldap libnotify lm_sensors mad mmx mng modules mp3 mp4 mpeg mplayer mudflap multilib mysql ncurses nls nptl nsplugin nvidia ocaml ocamlopt odbc ogg opengl openmp pam pango pcre pdf phonon plasma png policykit postgres ppds pppd python qt3support qt4 readline scanner sdl session smartcard smp snmp spell sqlite3 sse sse2 ssl startup-notification svg taglib tcpd theora threads tiff truetype type1 udev udisks unicode upower usb v4l2 vim-syntax vorbis wifi wxwidgets x264 xcb xcomposite xft xinerama xml xscreensaver xulrunner xv xvid xvmc zlib zsh-completion" ALSA_CARDS="ali5451 als4000 atiixp atiixp-modem bt87x ca0106 cmipci emu10k1x ens1370 ens1371 es1938 es1968 fm801 hda-intel intel8x0 intel8x0m maestro3 trident usb-audio via82xx via82xx-modem ymfpci" ALSA_PCM_PLUGINS="adpcm alaw asym copy dmix dshare dsnoop empty extplug file hooks iec958 ioplug ladspa lfloat linear meter mmap_emul mulaw multi null plug rate route share shm softvol" APACHE2_MODULES="actions alias auth_basic authn_alias authn_anon authn_dbm authn_default authn_file authz_dbm authz_default authz_groupfile authz_host authz_owner authz_user autoindex cache cgi cgid dav dav_fs dav_lock deflate dir disk_cache env expires ext_filter file_cache filter headers include info log_config logio mem_cache mime mime_magic negotiation rewrite setenvif speling status unique_id userdir usertrack vhost_alias" CALLIGRA_FEATURES="kexi words flow plan sheets stage tables krita karbon braindump" CAMERAS="ptp2" COLLECTD_PLUGINS="df interface irq load memory rrdtool swap syslog" ELIBC="glibc" GPSD_PROTOCOLS="ashtech aivdm earthmate evermore fv18 garmin garmintxt gpsclock itrax mtk3301 nmea ntrip navcom oceanserver oldstyle oncore rtcm104v2 rtcm104v3 sirf superstar2 timing tsip tripmate tnt ubx" INPUT_DEVICES="evdev keyboard mouse synaptics" KERNEL="linux" LCD_DEVICES="bayrad cfontz cfontz633 glk hd44780 lb216 lcdm001 mtxorb ncurses text" LIBREOFFICE_EXTENSIONS="presenter-console presenter-minimizer" PHP_TARGETS="php5-3" PYTHON_TARGETS="python3_2 python2_7" QEMU_SOFTMMU_TARGETS="i386 x86_64" QEMU_USER_TARGETS="i386 x86_64" RUBY_TARGETS="ruby18 ruby19" USERLAND="GNU" VIDEO_CARDS="nvidia" XTABLES_ADDONS="quota2 psd pknock lscan length2 ipv4options ipset ipp2p iface geoip fuzzy condition tee tarpit sysrq steal rawnat logmark ipmark dhcpmac delude chaos account" USE_PYTHON="2.7" Unset: CPPFLAGS, CTARGET, INSTALL_MASK, LC_ALL, LINGUAS, PORTAGE_BUNZIP2_COMMAND, PORTAGE_COMPRESS, PORTAGE_COMPRESS_FLAGS, PORTAGE_RSYNC_EXTRA_OPTS
$
On 19/09/2012 12:06, Mark Wright wrote:
Hi,
Thanks for your great work on polyml 5.5. I'd like to bump polyml in Gentoo portage, however this one test fails in the test suite:
./configure --prefix=/usr --build=x86_64-pc-linux-gnu --host=x86_64-pc-linux-gnu --mandir=/usr/share/man --infodir=/usr/share/info --datadir=/usr/share --sysconfdir=/etc --localstatedir=/var/lib --libdir=/usr/lib64 --disable-dependency-tracking --with-x --with-gmp --without-portable --with-threads
...
make tests
...
Test071.ML => Failed!!
Thanks for providing all the information and for your work on packaging Poly/ML for Gentoo. This particular test is the one that detects whether building the basis library has added a binding for "it". It shouldn't really although it's largely innocuous and I went through the library removing the cases where it did this but it seems I hadn't tested with the optional X-Windows/Motif library. I've now fixed that in SVN. However this raises the question as to why you have included the "with-x" option at all. Unless you have strong reasons to include it I would recommend not building with this. I doubt that many users will actually want the X-Windows system and building with this option will introduce many unnecessary dependencies.
However, while I was testing this I discovered a much more serious problem. It appears that --without-portable is actually being treated as --with-portable by the configure script and the only way to build the native code version is not to include the option at all. Again I've fixed this in SVN trunk and if this tests out I'll probably port this to the 5.5 fixes branch. Meanwhile though you need to avoid giving this option.
David
David Matthews David.Matthews@prolingua.co.uk writes:
On 19/09/2012 12:06, Mark Wright wrote:
Hi,
Thanks for your great work on polyml 5.5. I'd like to bump polyml in Gentoo portage, however this one test fails in the test suite:
./configure --prefix=/usr --build=x86_64-pc-linux-gnu --host=x86_64-pc-linux-gnu --mandir=/usr/share/man --infodir=/usr/share/info --datadir=/usr/share --sysconfdir=/etc --localstatedir=/var/lib --libdir=/usr/lib64 --disable-dependency-tracking --with-x --with-gmp --without-portable --with-threads
...
make tests
...
Test071.ML => Failed!!
Thanks for providing all the information and for your work on packaging Poly/ML for Gentoo. This particular test is the one that detects whether building the basis library has added a binding for "it". It shouldn't really although it's largely innocuous and I went through the library removing the cases where it did this but it seems I hadn't tested with the optional X-Windows/Motif library. I've now fixed that in SVN.
Hi David,
Neat, thanks!
However this raises the question as to why you have included the "with-x" option at all. Unless you have strong reasons to include it I would recommend not building with this. I doubt that many users will actually want the X-Windows system and building with this option will introduce many unnecessary dependencies.
On Gentoo we allow the users to configure with USE flags which options are selected. The polyml ebuild always had the X USE flag to control the -with-x option.
Currently that means the X use flag is likely to be enabled on desktop machines, and disabled on server machines.
Since you advise against it I'm wondering about removing it or somehow disabling it.
However, while I was testing this I discovered a much more serious problem. It appears that --without-portable is actually being treated as --with-portable by the configure script and the only way to build the native code version is not to include the option at all. Again I've fixed this in SVN trunk and if this tests out I'll probably port this to the 5.5 fixes branch. Meanwhile though you need to avoid giving this option.
David
I can help with the configure problem:
http://sources.gentoo.org/cgi-bin/viewvc.cgi/gentoo-x86/dev-lang/polyml/file...
Thanks, Mark
(resend to the list, sorry for the duplicate)
On 19/09/2012 14:54, Mark Wright wrote:
David Matthews David.Matthews@prolingua.co.uk writes:
However this raises the question as to why you have included the "with-x" option at all. Unless you have strong reasons to include it I would recommend not building with this. I doubt that many users will actually want the X-Windows system and building with this option will introduce many unnecessary dependencies.
On Gentoo we allow the users to configure with USE flags which options are selected. The polyml ebuild always had the X USE flag to control the -with-x option.
Currently that means the X use flag is likely to be enabled on desktop machines, and disabled on server machines.
Since you advise against it I'm wondering about removing it or somehow disabling it.
I haven't used Gentoo so I don't know how the packaging works there. I guess I was assuming that you were building binary packages in a similar way to Debian/Ubuntu. If there is only a single Poly/ML package then it's not a good idea to make it dependent on all the X-windows and Motif libraries. I did read somewhere, though, that in Gentoo you build from source. If that is true then enabling the X-Windows system is fine on platforms that already have the X-Windows/Motif libraries and headers present. Perhaps I should get the "check" option for --with-x to work correctly so that it is possible to build in the X-Windows support if everything is present but silently fall back to building without X if something is missing. This is roughly the way GMP support is done.
I can help with the configure problem:
http://sources.gentoo.org/cgi-bin/viewvc.cgi/gentoo-x86/dev-lang/polyml/file...
I wish I'd been aware of this earlier; I could have fixed the configure script before release.
Regards, David
David Matthews David.Matthews@prolingua.co.uk writes:
On 19/09/2012 14:54, Mark Wright wrote:
David Matthews David.Matthews@prolingua.co.uk writes:
However this raises the question as to why you have included the "with-x" option at all. Unless you have strong reasons to include it I would recommend not building with this. I doubt that many users will actually want the X-Windows system and building with this option will introduce many unnecessary dependencies.
On Gentoo we allow the users to configure with USE flags which options are selected. The polyml ebuild always had the X USE flag to control the -with-x option.
Currently that means the X use flag is likely to be enabled on desktop machines, and disabled on server machines.
Since you advise against it I'm wondering about removing it or somehow disabling it.
I haven't used Gentoo so I don't know how the packaging works there. I guess I was assuming that you were building binary packages in a similar way to Debian/Ubuntu. If there is only a single Poly/ML package then it's not a good idea to make it dependent on all the X-windows and Motif libraries. I did read somewhere, though, that in Gentoo you build from source.
Hi David,
Yes we build it from the source code. I bumped polyml to 5.5 in portage (as 5.5.0 since that is the version reported by poly -v). Isabelle 2012 built fine with polyml 5.5.
If that is true then enabling the X-Windows system is fine on platforms that already have the X-Windows/Motif libraries and headers present. Perhaps I should get the "check" option for --with-x to work correctly so that it is possible to build in the X-Windows support if everything is present but silently fall back to building without X if something is missing. This is roughly the way GMP support is done.
For Gentoo it is fine if the --with-x fails if something is missing.
I applied your Test071 fix, the tests pass with (and without) the X use flag, thanks.
I can help with the configure problem:
http://sources.gentoo.org/cgi-bin/viewvc.cgi/gentoo-x86/dev-lang/polyml/file...
I wish I'd been aware of this earlier; I could have fixed the configure script before release.
Regards, David
Sorry, guess I should have mentioned it earlier.
I applied your configure patch, thanks.
Thanks, Mark
On Thu, 20 Sep 2012, Mark Wright wrote:
I bumped polyml to 5.5 in portage (as 5.5.0 since that is the version reported by poly -v). Isabelle 2012 built fine with polyml 5.5.
Are you sure about this? Did you include the important libsha1.so that is part of the regular Isabelle2012 distribution of Poly/ML?
You probably know already that I am very sceptical about this packaging of Isabelle components as "native" OS packages. In so many years I've never seen a packaging that was right, and it is getting more and more difficult to achieve that with all the Isabelle add-ons that are now standard.
Makarius
Makarius makarius@sketis.net writes:
On Thu, 20 Sep 2012, Mark Wright wrote:
I bumped polyml to 5.5 in portage (as 5.5.0 since that is the version reported by poly -v). Isabelle 2012 built fine with polyml 5.5.
Are you sure about this?
Hi Makarius,
Proofs with proof-general and sledgehammer with e 1.6 and spass 3.7 work. The isabelle test suite returns a 0 exit status during the build. isabelle jedit works with a simple proof.
Did you include the important libsha1.so that is part of the regular Isabelle2012 distribution of Poly/ML?
No, thanks for letting me know I should, I guess I should build it from the source code here:
https://bitbucket.org/makarius
You probably know already that I am very sceptical about this packaging of Isabelle components as "native" OS packages. In so many years I've never seen a packaging that was right, and it is getting more and more difficult to achieve that with all the Isabelle add-ons that are now standard.
Makarius
The issues I know of:
- No source code to spass 3.8ds or later available. I would very much like to provide a more recent release of spass.
- Haskabelle does not compile with the current version of haskell-src-exts. Its on my todo list to ask the haskell-src-exts maintainers to consider adding the support for undefined pragmas.
- I have an ebuild for z3 integration with sledgehammer. I may not add that to portage though as it is packaging a binary. Gentoo's open source philosophy is to build packages from the source code.
I use Isabelle. I have added sci-mathematics/spass-3.7, sci-mathematics/e-1.6 and sci-mathematics/cvc3-2.4.1 to portage with isabelle use flags, that automatically create their settings files and add themselves to the isabelle components file.
I am prepared to fix issues and to add more Isabelle components to portage for those components that can be built from the source code.
Thanks, Mark
On Tue, 25 Sep 2012, Mark Wright wrote:
Did you include the important libsha1.so that is part of the regular Isabelle2012 distribution of Poly/ML?
No, thanks for letting me know I should, I guess I should build it from the source code here:
This is one of the clones floating around. The actual sources used to build Poly/ML are shipped with our standard polyml-5.4.1 archive, or now the polyml-5.5.0 components http://isabelle.in.tum.de/components/polyml-5.5.0.tar.gz
All these Isabelle components have a README that explains how it was built, and how it can in principle be reconstructed independently, although that is a lot of redundant work.
I use Isabelle. I have added sci-mathematics/spass-3.7, sci-mathematics/e-1.6 and sci-mathematics/cvc3-2.4.1 to portage with isabelle use flags, that automatically create their settings files and add themselves to the isabelle components file.
I am prepared to fix issues and to add more Isabelle components to portage for those components that can be built from the source code.
An impressive amount of work just to make things conformant to Gentoo. You also seem to be exceptional in using the result yourself, unlike many Linux hobbyists who merely package things and let the world stumble on the problems of the result.
Nonetheless, you will always be one step behind the real Isabelle distribution. Next time we depend essentially on Java 7 with JavaFX from Oracle, and I can't say how far the OpenJDK version of that is.
In the end the main question is how to serve users best. There is hardly anybody missing a Debianized version of Isabelle, but people occasionally come to me and say I should bundle even more things in the one big Isabelle distribution, bypassing problems of their standard OS packages.
Makarius
Makarius> In the end the main question is how to serve users best. Makarius> There is hardly anybody missing a Debianized version of Makarius> Isabelle, but people occasionally come to me and say I should Makarius> bundle even more things in the one big Isabelle distribution, Makarius> bypassing problems of their standard OS packages.
Here is one datapoint the other way. I wish Isabelle was DFSG free and I wish it was possible to package it. I will not use the binary bundle, just as I will not use a binary bundle of, say, Adobe Reader, however convenient it might seem at any given moment.
I would be interested to know what the "problems of their standard OS packages" are, in the case of Debian.
I feel I must echo Ian Zimmerman's sentiment! (Although I don't use Debian or Isabelle much.) I will be updating the Arch Linux AUR package for HOL4 when the new release comes out, and might allocate some spare time to working on an Isabelle package for Arch Linux if anyone expresses interest (and hopefully collaboration :)).
On Wed, Sep 26, 2012 at 5:43 PM, Ian Zimmerman itz@buug.org wrote:
Makarius> In the end the main question is how to serve users best. Makarius> There is hardly anybody missing a Debianized version of Makarius> Isabelle, but people occasionally come to me and say I should Makarius> bundle even more things in the one big Isabelle distribution, Makarius> bypassing problems of their standard OS packages.
Here is one datapoint the other way. I wish Isabelle was DFSG free and I wish it was possible to package it. I will not use the binary bundle, just as I will not use a binary bundle of, say, Adobe Reader, however convenient it might seem at any given moment.
I would be interested to know what the "problems of their standard OS packages" are, in the case of Debian.
-- Ian Zimmerman gpg public key: 1024D/C6FF61AD fingerprint: 66DC D68F 5C1B 4D71 2EE5 BD03 8A00 786C C6FF 61AD http://www.gravatar.com/avatar/c66875cda51109f76c6312f4d4743d1e.png Rule 420: All persons more than eight miles high to leave the court. _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
-
David.Matthews＠prolingua.co.uk -
gienah＠gentoo.org -
itz＠buug.org -
makarius＠sketis.net -
ramana.kumar＠gmail.com