[MetaPRL Users] Term extraction problem

[Wojtek Moczydlowski]

On Wed, 6 Sep 2006, Aleksey Nogin wrote:

> Hm, this is very strange. Could you try to upgrade to the most recent version 
> of MetaPRL?
>
> The procedure is the following:
>
> 1) Optional: for every every theory where you have proof that you care to 
> preserve, run
>
> cd "/theory_name"
> export ()
>
> in MetaPRL.
>
> 2) Delete all the *.cmiz, *.cmoz and *.prlb files in the MetaPRL tree (you 
> can do this by running "omake realclean").
>
> 3) Run "svn up" in the root of the MetaPRL tree (you need to do this step on 
> a machine that has subversion installed).
>
> 4) Run "omake" to build it.
>
> Aleksey
>
> P.S. This is not normally this complicated - the steps (1) and (2) are only 
> needed because the binary representations of the proofs were changed very 
> recently, so any proofs that need to be preserved have to be exported to a 
> stable textual representation (step 1) and all the old proof binaries need to 
> be deleted (step 2).

Well, I don't have any proofs yet to save. But, unfortunately, even after
this I still get the same message. Maybe the information that even when I complete the proof
and * appears everywhere, after I quit and come back to the editor, the *
disappears and only ? remaing is useful?

Wojtek