[MLton] MLton HOL

Wed, 14 Jul 2004 12:27:42 -0700

> today I checked out the MLton source from the cvs repository, and 
> managed to build everything (using MLton 20040227 to bootstrap).

Glad to hear this works.  It should make testing improvements easier.

> Before trying the full psl executable, I thought I'd give the new 
> compiler a go on a smaller (220,000 line) test incorporating all of 
> the HOL theory files. Unfortunately I'm still getting the
> 
> sfwrite failed (No space left on device)
> 
> error, which I assume is the compiler running out of memory on the 4Gb 
> machine I'm using.

Sort of.  What it means is that the runtime was trying to mmap a
bigger heap and wasn't able to, so it's trying to write the entire
current heap to a file (in /tmp or TMPDIR), munmapping the heap, and
trying again.  The sfwrite failure occured because there wasn't enough
disk space in /tmp to write the heap.  I thought you had this problem
before and worked around it by setting TMPDIR to somewhere that had
lots of disk space.  Did you have TMPDIR set for this run?

>              num functions 6207
>              num blocks 421043
>              num statements 423273
>              main num vars: 524665
>              main num blocks: 325474
>              inline starting

Interesting stats.  These are very different numbers than we saw for
psl1.sml.  Here are some numbers I have lying around from a compile of
psl1 that I ran on July 1.

	    num functions 4891
	    num blocks 97622
	    num statements 451242
	    main num vars: 82220
	    main num blocks: 28474
	    inline starting

So, metis-test has factor of 4.5 more blocks and a factor of 6 more
vars in main.  Either the compiler has changed significantly in the
interim (unlikely) or this is a very different program (likely).  Of
course we will have to fix the problems here, but my main point is
that the failure to compile metis-test may not be indicative of
problems in compiling psl1.

I did a run with plenty of space in /tmp, and was able to get past
inlining

	    post.ssa size is 110,269,032 bytes
...
	    inline starting
	    inline finished in 31.74 + 680.72 (96% GC)
	    post.ssa size is 451,475,020 bytes

But, as the sizes show, something bad is happening -- a factor of four
blowup is unnacceptable (and unseen before).  Furthermore, this blowup
causes a later optimization pass (localRef) to choke.

To see if I could get a compile to succeed, I compiled with 

	-drop-pass inline

This did succeed, but quite painfully.  Here were the timings.

	 machine size is 768,275,708 bytes
      pre codegen finished in 8663.92 + 1209.54 (12% GC)
      x86 code gen finished in 29226.72 + 5749.49 (16% GC)
   Compile SML finished in 37890.81 + 6959.03 (16% GC)
   Compile C and Assemble finished in 159.43 + 0.00 (0% GC)
   Link finished in 12.60 + 0.00 (0% GC)
MLton finished in 38063.34 + 6964.43 (15% GC)
...
max live: 1,950,400,964 bytes
max semispace: 2,028,421,120 bytes

Twelve and a half hours!  Blech.  And the machine IL size going into
the codegen is about three times larger than when compiling psl1.
That jibes with the factor of 4.5 we saw for blocks.  The size of the
final executable is also huge: 82,087,840 bytes.

I am afraid to say that the performance does not look easy to fix.  I
will continue to work on it, but I think your best bet for now is to
figure out how to move the automatically generated theories out of the
code.

FYI, here is the output from running the executable.

<<HOL message: Couldn't define encode function for type string>>
<<HOL message: Couldn't define encode function for type semi_ring>>
<<HOL message: Couldn't define encode function for type ring>>
<<HOL message: Couldn't define encode function for type deep_form>>
<<HOL message: loading RealArith>>

-----------------------------------------------------------------
       HOL-4 [Kananaskis 3]

       For introductory HOL help, type: help "hol";
-----------------------------------------------------------------

<<HOL warning: Parse.Term: Grammar ambiguous on token pair rem and rem, and probably others too>>

--------------------------------------------------------------------------

Syntax checking the problem sets

TRUE
JH_test
CYCLIC
MN_bug
RELATION_COMPOSITION
PROP_1
PROP_2
PROP_3
PROP_4
PROP_5
PROP_6
PROP_7
PROP_8
PROP_9
PROP_10
PROP_11
PROP_12
PROP_13
PROP_14
PROP_15
PROP_16
PROP_17
MATHS4_EXAMPLE
LOGICPROOF_1996
XOR_ASSOC
ALL_3_CLAUSES
CLAUSE_SIMP
P18
P19
P20
P21
P22
P23
P24
P25
P26
P27
P28
P29
P30
P31
P32
P33
P34
P35
P36
P37
P38
P39
P40
P41
P42
P43
P44
P45
P46
P50
LOGICPROOF_L10
LOGICPROOF_1999
P55
P57
P58
P59
P60
GILMORE_1
GILMORE_2
GILMORE_3
GILMORE_4
GILMORE_5
GILMORE_6
GILMORE_7
GILMORE_8
GILMORE_9
GILMORE_9a
BAD_CONNECTIONS
LOS
STEAM_ROLLER
MODEL_COMPLETENESS
REFLEXIVITY
SYMMETRY
TRANSITIVITY
TRANS_SYMM
SUBSTITUTIVITY
CYCLIC_SUBSTITUTION_BUG
JUDITA_1
JUDITA_1'
JUDITA_2
JUDITA_2'
JUDITA_3
INJECTIVITY
INJECTIVITY2
SELF_REWRITE
P48
P49
P51
P52
UNSKOLEMIZED_MELHAM
CONGRUENCE_CLOSURE_EXAMPLE
EWD
EWD'
JIA
WISHNU
AGATHA
DIVIDES_9

Exception raised at matchTools.unify_type:
different type constructors
unhandled exception: HOL_ERR: {origin_structure = matchTools,
  origin_function = unify_type,
  message = different type constructors}

real	7m21.717s
user	7m20.880s
sys	0m0.570s