[MetaPRL Users] How to save a proof ?

[Aleksey Nogin]

On 17.06.2007 15:30, Sunil Kothari wrote:

> I get the following error message when I try to save the proof.
> 
> Saving myw_list
> Invalid Argument:
> Invaoutput_value: functional value
> Refine_exn.ToploopIgnoreExn(_)
> 
Sunil,

Yes, unfortunately there is a bug with functional values in some saved 
proofs and so far we were unable to track it down.

However, there is a workaround - use "export" instead of "save" whenever 
"save" fails (and then delete the corrupted .prlb file). The export 
function dumps an ASCII representation of the proof into the .prla file 
and is free of the "functional value" problem. The "export" function 
could be much slower than "save", which is the reason it is not used by 
default.

Hope this helps.

Aleksey

-- 
Aleksey Nogin, Research Scientist
Advanced Technologies Department, Information & System Sciences Lab
HRL Laboratories, LLC, Malibu, CA