Hi Amy, Please email me directly for support on OpenTheory, since the project is still in an early stage of development and there are currently few users.
Firstly, take a look at the documentation in http://www.gilith.com/software/opentheory/notes.html In particular, the frequently asked question list might help to answer some of your questions about getting the tool working. If that doesn't help, please send me a private email with more details about what you're trying to do, and I'll see if I can help with pointers or bugfixes. Cheers, Joe 2010/3/23 anythingroom <anythingr...@126.com>: > Hi， > > 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? > > And now I can’t read the proof article file into my theorem > prover(HOL4).Before I read your paper entitled “OpenTheory: Package > Management for Higher Order Logic Theories”, it was reference to “These HOL > Light theories were read into HOL4 by a tool for reading articles > implemented by Quinn Yee Qin The.”Can you tell me the method about “How can > I use the tool of reader read the proof article file?” > > I'm looking forward for your reply. Thank you very much! > > Best wishes, > > Amy > > > > > ------------------------------------------------------------------------------ > 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 > > ------------------------------------------------------------------------------ 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
