Yuhui,

On 22 Feb 2013, at 14:24, Yuhui Lin wrote:

> Hi,
> 
> I wonder if is possible to load proof power from polyML directly, perhaps by 
> PolyML.make with the proof power source code.

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. 

> 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.  
> 

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.

Regards,

Rob.


_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to