[ProofPower] ml library functions from pp command line

2013-02-22 Thread Yuhui Lin
Hi, I'm trying to build a programme on the top of proof power with the pp interface. I need a full polyML library from the pp interface, but I can't use some functions which are defined in polyML, e.g List.exists. Any suggestion ? Thanks in advance. best, Yuhui -- The University of Edinburgh

Re: [ProofPower] ml library functions from pp command line

2013-02-22 Thread Mark
That's because ProofPower overwrites PolyML's ML structure List with its own, for holding theory about HOL lists. I'm not sure if anything can be done about this without alterning the ProofPower build process (and, say, creating a copy of PolyML's List with a name not used by ProofPower). Mark.

Re: [ProofPower] ml library functions from pp command line

2013-02-22 Thread Rob Arthan
Mark, Yuhui, On Feb 22, 2013, at 12:47 PM, "Mark" wrote: > That's because ProofPower overwrites PolyML's ML structure List with its > own, for holding theory about HOL lists. I'm not sure if anything can be > done about this without alterning the ProofPower build process (and, say, > creating a

[ProofPower] load proof power with PolyML

2013-02-22 Thread Yuhui Lin
Hi, I wonder if is possible to load proof power from polyML directly, perhaps by PolyML.make with the proof power source code. 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

Re: [ProofPower] load proof power with PolyML

2013-02-22 Thread Rob Arthan
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 l

Re: [ProofPower] load proof power with PolyML

2013-02-22 Thread Yuhui Lin
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 wrote: > Yuhui, > > On 22 Feb 2013, at 14:24,