Poly/ML June 2020

polyml@lists.polyml.org

4 participants
4 discussions

Compiler (0ad5aa87) raises Option
by Michael.Norrish＠data61.csiro.au 10 Jul '20

10 Jul '20

I don't expect this in isolation will help, but the following HOL function causes the compiler to emit a Fail "Exception- Option unexpectedly raised while compiling" message. ?- - - fun EXISTS_SEP_REWRITE_RULE rw th = let (* possibly fragile *) val (p,q) = dest_eq (concl (SPEC_ALL rw)) val frame = genvar(type_of p) val vs = list_dest dest_sep_exists p val lhs = mk_star(last vs,frame) val vs = butlast vs fun find_exists_match lhs tm = let val (v,t) = dest_sep_exists tm val vs = list_dest dest_sep_exists tm in (butlast vs,last vs,generic_star_match [] lhs (last vs)) end fun find_term_and_apply f tm = f (find_term (can f) tm) fun foo th = let val (ws,tm,s) = find_term_and_apply (find_exists_match lhs) (concl th) val (t,t2) = (dest_eq (concl (SPEC_ALL rw))) val zs = list_dest dest_sep_exists t val (zs,z) = (butlast zs,list_dest dest_star (last zs)) val xs = list_dest dest_star tm val ys = filter (fn y => not (tmem y (map (subst s) z))) xs val t3 = foldr mk_sep_exists (subst s (list_mk_star z (type_of frame))) (map (subst s) zs) val goal = foldr mk_sep_exists (list_mk_star (t3::ys) (type_of frame)) ws val goal = mk_eq(foldr mk_sep_exists tm ws,goal) val lemma = auto_prove "EXISTS_SEP_REWRITE_RULE" (goal, SIMP_TAC std_ss [GSYM rw] THEN SIMP_TAC (std_ss++sep_cond_ss) [SEP_CLAUSES] THEN CONV_TAC (BINOP_CONV SEP_EXISTS_AC_CONV) THEN SIMP_TAC (std_ss++star_ss) [AC CONJ_ASSOC CONJ_COMM]) val lemma = CONV_RULE (RAND_CONV (ONCE_REWRITE_CONV [rw] THENC SIMP_CONV std_ss [SEP_CLAUSES])) lemma in foo (RW1 [lemma] th) end handle HOL_ERR _ => th in foo th end; - - - This comes from HOL4's examples/machine-code/hoare-triple/helperLib.sml (line 667 onwards). I will try to reduce it to a smaller instance. Michael

4 8

Horrific GC(?) behaviour in 5.8 (g44efa473)
by Michael.Norrish＠data61.csiro.au 21 Jun '20

21 Jun '20

I have some HOL code that runs to completion in ~24 seconds user time. On 5.7.1 it runs in about that much wall clock time too. (Unfortunately, this test is running on a different machine, necessarily, but this is an old Linux desktop which is far less powerful than the new Macbook Pro which is running 5.8.) On 5.8 (updated for MacOS Catalina to the SHA above), wall clock time is 8 minutes. The relevant code is the selftest in examples/miller/miller which is a big arithmetic normalisation. On the Mac, memory consumption (as reported by the Activity Monitor) gets as high as 20GB; on the Linux machine running 5.7.1, the consumption remains very slight (top reports 3% in its %MEM column; the machine has 16GB) Michael

4 8

GC followup
by Michael.Norrish＠data61.csiro.au 16 Jun '20

16 Jun '20

I instrumented the test regime to flag test cases where the GC time was more than 20% of the ?user time. I ran the same test on Linux 5.7.1 and the Mac Catalina machine. As per screenshot (Linux on left, Mac on right; user times in parentheses, gc times in seconds in red), the 5.8 GC is definitely worse. (I appreciate that occasionally the GC will kick in with "bad" times during a long series of very quick tests; I expect this explains the "bad" time in the Linux series.) I'm using Timer.getCPUTimer to get these measurements, getting nongc.usr and gc.usr. Michael

1 0

Poly/ML software directory
by David.Matthews＠prolingua.co.uk 04 Jun '20

04 Jun '20

After the discussion about a random number library I've been thinking about how to implement a repository or register of similar things. At the moment a repository containing the actual code seems too much but a directory or register looks like it could be useful. I've set up a database and associated web pages for a directory of software for Poly/ML. Rather than maintain all the data myself I'm asking anyone who has a library, application, sample code or anything else to register with the site and add the appropriate entries. As a starting point I've made an entry for the Windows GUI library that is currently included in the Poly/ML distribution but which I've now pulled out into a separate repository on Github. This is a bit of an experiment and I don't know how useful it will turn out to be. The web pages themselves could do with being improved but they should be in a state for beta-testing. I've selected fields based on what I think would be useful but they can always be changed. The web site is at https://www.polyml.org/software/index.php and is linked from the main Poly/ML website at www.polyml.org. Let me know what you think. David

2 3

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

Poly/ML June 2020