Thanks, now I see something useful: $ echo foo | ./munge.exe
The exported object file has version 5.71 but this library supports 5.70 (then it hangs) I have Poly/ML 5.7 installed in /usr/local (by Homebrew on Mac OS X 10.11), and the new 5.7.1 manually installed into $HOME. So I guess, when building `munge.exe` it must have been linked with libpolyml.a (or libpolymain.a) in /usr/local/lib because I didn’t put $HOME/lib into DYLD_LIBRARY_PATH (LD_LIBRARY_PATH on Linux). After completely removing Poly/ML 5.7 and rebuilding and installing 5.7.1 into /usr/local, the problem is resolved. Now munge.exe works correctly on my side. P. S. but multiple copies of Poly/ML actually worked well in all other cases, I normally use Poly/ML 5.6 (installed into a dedicated directory) to build HOL4 K11 release but never needed to build and run munge.exe from that version. Any way, sorry for disturbing. Regards, Chun > Il giorno 21 nov 2017, alle ore 12:18, [email protected] ha > scritto: > > Those that passed are not tests of the munger per se: they are building the > necessary background theories, and the munger executables. Those tests that > you are trying to run are actually trying to execute the mungers. > > If you test a munger interactively with > > $ echo foo | ./munge.exe > > what do you see? > > Michael > > On 21/11/17, 19:52, "Chun Tian" <[email protected]> wrote: > > Hi, > > I rebuilt again with -t option. By default Holmake have 4 parallel > threads, now all are blocked by munge tests: > > 501 60326 60299 0 9:48am ttys000 0:00.00 /bin/sh -c ./tymunge.exe > < tyabb_input > tyabb_output > 501 60327 60326 0 9:48am ttys000 0:00.00 ./tymunge.exe > 501 60330 60299 0 9:48am ttys000 0:00.00 /bin/sh -c ./munge.exe < > input > output > 501 60331 60330 0 9:48am ttys000 0:00.00 ./munge.exe > 501 60332 60299 0 9:48am ttys000 0:00.00 /bin/sh -c ./utymunge.exe > < tyabb_input > utyabb_output > 501 60333 60332 0 9:48am ttys000 0:00.00 ./utymunge.exe > 501 60334 60299 0 9:48am ttys000 0:00.00 /bin/sh -c ./munge.exe < > gh242_input > gh242_output > 501 60335 60334 0 9:48am ttys000 0:00.00 ./munge.exe > > However some munge tests indeed passed: > > Building directory src/TeX/theory_tests [21 Nov, 09:48:01] > Recursively calling Holmake in /Users/binghe/ML/HOL.stdknl/tools/cmp > Finished recursive invocation in /Users/binghe/ML/HOL.stdknl/tools/cmp > tyabbrevTheory > OK > foo248Theory > OK > bag248Theory > OK > mdtTheory > OK > untyabbrevTheory > OK > pp248Theory > OK > tymunge.exe > OK > munge.exe > OK > utymunge.exe > OK > munge248.exe > OK > > Regards, > > Chun Tian > >> Il giorno 21 nov 2017, alle ore 03:57, [email protected] ha >> scritto: >> >> Does HOL build with the -t option? >> >> This does some testing of the munging technology. >> >> Michael >> >> On 21/11/17, 10:03, "polyml on behalf of Chun Tian" >> <[email protected] on behalf of [email protected]> wrote: >> >> Hi Ramana, >> >> I found that “munge.exe” (generated from theories) doesn’t work with this >> new Poly release: it simply hangs when converting *.htex to *.tex files … >> and when I switched back to poly 5.6, it worked again. >> >> Can you confirm this on your side? >> >> —Chun >> >>> Il giorno 20 nov 2017, alle ore 22:58, Ramana Kumar >>> <[email protected]> ha scritto: >>> >>> The 5.7.1 candidate appears to work for HOL4 and CakeML - I haven't done >>> extensive tests, but normal builds seem fine. >>> >>> On 21 November 2017 at 08:41, Makarius <[email protected]> wrote: >>> On 20/11/17 14:23, David Matthews wrote: >>>> Thanks to everyone who sent in bug reports. We're almost ready to >>>> release 5.7.1. I've updated Git master ( 44b7b88 ) with pre-built >>>> compilers for 5.7.1. This is the last chance check it before the >>>> release which will probably happen at the end of the week. >>> >>> I have successfully built this version on Linux, Windows, mac OS, and >>> ran vorious manual tests of Isabelle + AFP. It all looks fine. >>> >>> Note that I will be on travel on Wed--Fri this week, so if there are any >>> last-minute issues, I cannot do any tests during these days. >>> >>> >>> Makarius >>> >>> _______________________________________________ >>> polyml mailing list >>> [email protected] >>> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml >>> >>> _______________________________________________ >>> polyml mailing list >>> [email protected] >>> http://lists.inf.ed.ac.uk/mailman/listinfo/polyml >> >> >> > > >
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
