Hi Rob,

Thanks for you reply. You're right, ProofPower doesn't have to be in the 
middle, as there is no dependency.  Could you give me some hint about how to 
build ProofPower + some_libraries ? 


On 22 Feb 2013, at 14:41, Rob Arthan <r...@lemma-one.com> wrote:

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

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Proofpower mailing list

Reply via email to