Dear Dr. Michael Norrish, Yes, I was working on it on this Feb. And I appreciate the help from both Dr. Joe Hurd and you.
Unfortunately, I could not use this reader successfully since there was no input .art file to make the reader running normally. What I have done was to modify the related lines and copy a file generated from opentheory as the input file, then try to run the reader. However, the output was an empty .out file, which exists without any content. When I tried to get any example from the designer (Mr.Yee Qin Teh) of this reader, he could not provide any of it since it was a project he had done few years ago. And I also found the problem on transferring a large .ml file the same as Amy's case. But I could not solve it. Later on, I found my research work can be developed without matrix theory temporarily. Thus, I stopped there and continue my research work until now. If Amy needs help, I can provide some of my experience and lessons on testing this reader. And I would like to learn SourceForge during part time. Thanks again! Best Wishes, Liya Quoting Michael Norrish <michael.norr...@nicta.com.au>: > 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
