<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">Yuhui,<div><br><div><div>On 22 Feb 2013, at 14:24, Yuhui Lin wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div>Hi,<br><br>I wonder if is possible to load proof power from polyML directly, perhaps by PolyML.make with the proof power source code. </div></blockquote><div><br></div>I have never tried PolyML.make. There is no reason why you shouldn't compile the ProofPower source code by loading it in from a Poly/ML session, but I suspect that there are various things that might not work properly without some adjustment if you were to do that. </div><div><br><blockquote type="cite"><div>The fact is that we want to build a system which proof power will be in the middle of the architecture, i.e some_libraries <-- proofpower <-- another_component_with_UI. <br><br></div></blockquote><br></div><div>Do you mean you want to construct one ML program that includes the source of some_libraries, plus the source of ProofPower, plus the source of another_component_with_UI. If so, then why does ProofPower need to be in the middle? That would only make a difference if some_libraries was providing replacements for functions that ProofPower uses, wouldn't it? In any case, it sould be a relatively simple change to make the starting point of the ProofPower build be Poly/ML + some_libraries.</div><div><br></div><div>Regards,</div><div><br></div><div>Rob.</div><div><br></div><br></div></body></html>