Re: [Isarmathlib-devel] (solved) How to configure Isabelle to use IsarMathLib

[Victor Porton]

05.01.2011, 15:35, "Victor Porton" <address@hidden>:
> 05.01.2011, 13:24, "Slawomir Kolodynski" <address@hidden>;:
>
>>  --- On Tue, 1/4/11, Victor Porton <address@hidden>;; wrote:
>>>   How to make Isabelle and ProofGeneral to use IsarMathLib? I
>>>   want to import theories from IsarMathLib and make use of
>>>   "Find Theorems" feature of ProofGeneral.
>>  Start ProofGeneral in the IsarMathLib directory (where the theory files 
>> are).
>>  In your file write
>>
>>  theory mytheory imports func1
>>
>>  and process that. That will check and make available for searching 
>> IsarMathLib's func1.thy and all theory files that depend on it.
>>
>>  There is an alternative method where you create a "heap image". This is 
>> like a binary with all proven theorems. You use it by selecting from 
>> ProofGeneral instead of ZF logic. The method is described at 
>> http://www.cl.cam.ac.uk/research/hvg/Isabelle/faq.html .
>>  I haven't used it for a long time.
>
> I did
> $ isabelle usedir -b ZF ../../IsarMathLib
>
> and afterward (from the directory ../..):
> $ isabelle emacs -p xemacs21 -l IsarMathLib
>
> theory my
>   imports Fol1
> begin
> end
>
> *** Could not find theory file "Fol1.thy" in ".", "/home/porton/math/formal"
> *** Theory loader: the error(s) above occurred while examining theory "Fol1"
> *** At command "theory".
>
> It does not work.

This was not working because there were selected ZF in ProofGeneral as default.

Now I removed this preference and a new problem appeared:

$ isabelle emacs -p xemacs21 -l IsarMathLib 

When I try to verify:

Unknown logic "IsarMathLib" -- no heap file found in:
  /home/porton/.isabelle/heaps/Isabelle2009-2/polyml-5.3.0_x86-linux
  /usr/local/stow/Isabelle2009-2/heaps/polyml-5.3.0_x86-linux

Oh, it works with:

$ isabelle emacs -p xemacs21 -l ./IsarMathLib 

-- 
Victor Porton - http://portonvictor.org