5.7.1 release candidate - Poly/ML

21 Nov 2017

      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, Michael.Norrish at data61.csiro.au 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" <binghe.lisp at gmail.com> 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, Michael.Norrish at data61.csiro.au 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" <polyml-bounces at inf.ed.ac.uk on behalf of binghe.lisp at gmail.com> 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 <Ramana.Kumar at cl.cam.ac.uk> 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 <makarius at sketis.net> 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
polyml at inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

polyml mailing list
polyml at inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml