[MetaPRL Users] Term extraction problem

[Aleksey Nogin]

On 06.09.2006 08:39, Wojtek Moczydlowski wrote:

> It repeatedly refuses to work for me :) even for the test files attached
> (and renamed to wojtek1):

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