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 ?
best, Yuhui On 22 Feb 2013, at 14:41, Rob Arthan <[email protected]> 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 [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
