On 24/03/10 01:30, anythingroom wrote:
I have been generated a proof article file from a HOL Light theory file.
But I found that the opentheory can??t use the large .ml file to generate
the proof articles,for example vector.ml.When I run the command
??opentheory compile??,the screen appeard the erroe of ??out of memory??.Can
you tell me why and how to solve it please?
It sounds like you will have to debug your OpenTheory reader. I think Liya Liu
<liy_...@encs.concordia.ca> is working on the code that was used in the article
you mention for HOL4 (by Yee Qin Teh). If this is also the code you are using,
perhaps you two should coordinate.
Let me know if you'd like to work together using SourceForge (it would be no
problem to make you both developers).
Michael
------------------------------------------------------------------------------
Download Intel® Parallel Studio Eval
Try the new software tools for yourself. Speed compiling, find bugs
proactively, and fine-tune applications for parallel performance.
See why Intel Parallel Studio got high marks during beta.
http://p.sf.net/sfu/intel-sw-dev
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
