Hi Michael,
Well, the datatypes were not that huge. But there was a definition that
used "deep pattern matching", that I think was the culprit:
val _ = Define `
dest_Call (cl,(fs:context list)) =
(* to avoid returning an option type, since a dest_Call can never be
a ret *)
let failwith s = ([],LT_Ret(failwith s)) in
case (cl,fs) of
(Cl(e,env),Ref(Wrap Hole)::fs) ->
if is_vval e then (fs,LT_Ref(Cl(e,env))) else failwith "dest_Ref"
|| (Cl(Loc l,_1),Deref(Wrap Hole)::fs) -> (fs,LT_Deref(l))
|| (Cl(Loc l,_2),Assign(Wrap Hole,Wrap(Clo(Cl(v2,env2))))::fs) ->
(fs,LT_Assign(l,Cl(v2,env2)))
|| (Cl(Const "Mutex.create",_3),
App(Wrap Hole,Wrap(Clo(Cl(Const "unit",_4))))::fs) -> (fs,LT_Create)
|| (Cl(Const "Mutex.lock",_5),
App(Wrap Hole,Wrap(Clo(Cl(Variant("Mut",Int m),_6))))::fs) ->
(fs,LT_Lock(m))
|| (Cl(Const "Mutex.unlock",_7),
App(Wrap Hole,Wrap(Clo(Cl(Variant("Mut",Int m),_8))))::fs) ->
(fs,LT_Unlock(m))
|| (Cl(Const "Condition.create",_9),
App(Wrap Hole,Wrap(Clo(Cl(Const "unit",_))))::fs) -> (fs,LT_CCreate)
|| (Cl(Const "Condition.wait",_a),
App(Wrap Hole,Wrap(Clo(Cl(Variant("Cond",Int c),_b))))::
App(Wrap Hole,Wrap(Clo(Cl(Variant("Mut",Int m),_c))))::fs) ->
(fs,LT_Wait(m,c))
|| (Cl(Const "Condition.broadcast",_d),
App(Wrap Hole,Wrap(Clo(Cl(Variant("Cond",Int c),_e))))::fs) ->
(fs,LT_Broadcast(c))
|| (Cl(Const "File.write",_f),
App(Wrap Hole,Wrap(Clo(Cl(String(fn),_g))))::
App(Wrap Hole,Wrap(Clo(cl)))::fs) ->
(fs,LT_FWrite(fn,string_list_of cl))
|| (Cl(Const "File.read",_h),
App(Wrap Hole,Wrap(Clo(Cl(String(fn),_i))))::fs) -> (fs,LT_FRead(fn))
|| (Cl(Const "Messaging.listen",_j),
App(Wrap Hole,Wrap(Clo(Cl(Variant("Ip",Int ip),env1))))::
App(Wrap Hole,Wrap(Clo(Cl(Variant("Port", Int
port),env2))))::fs) -> (fs,LT_Listen(ip,port))
|| (Cl(Const "Messaging.connect",_k),
App(Wrap Hole,Wrap(Clo(Cl(Variant("Ip",Int ip),env1))))::
App(Wrap Hole,Wrap(Clo(Cl(Variant("Port",Int port),env2))))::fs)
-> (fs,LT_Connect(ip,port))
|| (Cl(Const "Messaging.send",_l),
App(Wrap Hole,Wrap(Clo(Cl(Variant("Conn",Int c),_m))))::
App(Wrap Hole,Wrap(Clo(Cl(String s,_n))))::fs) -> (fs,LT_Send(c,s))
|| (Cl(Const "Messaging.recv",_o),
App(Wrap Hole,Wrap(Clo(Cl(Variant("Conn",Int c),_p))))::fs) ->
(fs,LT_Recv(c))
|| _q -> failwith "dest_Call"
`;
I changed the definition so that it first case splits on e, then on fs.
This seems to have solved the problem, and cut about 3 mins off my
compile time.
This defn. is actually ported from a Caml defn, where such deep pattern
matching is fairly common.
I have no idea what hol's pattern matching code is doing (I haven't even
looked at what the defn. actually produces in raw hol), but are there
obvious things that could be done to improve this part of the code?
Also, I don't quite understand why the system should give an "out of
memory" error. It is true that my 2GB of memory were exhausted, but
shouldn't the system then start swapping? I watched the system monitor
(xosview), and it showed memory usage gradually rising to 2GB, at which
point hol died. I don't suppose it really matters now.
T
Michael Norrish wrote:
> Tom Ridge wrote:
>> Dear All,
>>
>> I see the following when compiling some theories:
>>
>> Exporting theory "exp" ...
>> Failure while writing theory!
>> Fatal error: out of memory.
>>
>> I'm sure I've got enough memory. How can I tell hol/mosml to use more?
>
> Ouch. How huge is the datatype definition hiding inside expScript.sml?
>
> Michael.
>
-------------------------------------------------------------------------
Check out the new SourceForge.net Marketplace.
It's the best place to buy or sell services for
just about anything Open Source.
http://ad.doubleclick.net/clk;164216239;13503038;w?http://sf.net/marketplace
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
