Re: [CZT-Devel] CZT Tool Install and execute from c++

[Leo F. <leo...@ne...>]

Hi Petra,

That's very helpful, thank you. It doesn't happen with my build, but I think I figured out why it does on yours.
The way to check if we are talking about the same problem is to clean and build, and it shouldn't happen.
Notice that the need for the clean-install maybe needed for other reasons, like out-of-memory when handling
too many (large) tests as a result of the extra tests created on the fly.

Cutting a long story short, the reason for this is because of a combination of factors: ZEves proof keywords use in declarations;
special names only allowed by the prover; CZT markup translations (e.g., Latex->Unicode->Latex); Latex markup directive handling, etc.

The source of the problem is when translating from tex-zed8, then back from zed8->tex. The issue is with ZEves use of "proof" keywords 
in "special" declared names (E.g., names only the prover can declare - containing $). They can be used in expressions/predicates, though. 
The issue is that the Unicode2Latex doesn't add necessary hardspaces for this(ese) kind of names. That is, in Latex

(R \cup S) ~applies\$to~ x

(as in appTo.tex) leads to this in Unicode when converted from Latex

( R ∪ S ) applies$to x 

which then leads to this when converted back to Latex (from Unicode)

(R \cup S) applies\$to x

because applies$to is an infix function (operator template), then no hard spaces is added. 
The overall solution I added was to force this special case at the Unicode2Latex markup printer, 
such that these case gets handled properly. 

Also, notice that the problem only happens if you use the zed8->tex printer for this peculiar operator template.... 
ZEves makes a poor naming convention here, I should say. All should be okay now.

Thanks for spotting this.
Leo

On 10 Oct 2011, at 12:55, Petra Dietrich wrote:

> Hi Leo,
> 
> That's better; I can now see the error messages.
> See below what maven prints and attached the detailed report for
> ProofScriptParsingTest.
> 
> Cheers,
> Petra
> 
> Running net.sourceforge.czt.parser.zeves.ProofScriptParsingTest
> Number of tests for Z/Eves proofs parsing: 121
> 
> Encountered exception during reparsing
> net.sourceforge.czt.session.CommandException
> 
> Unexpected exception
> 	File     :
> file:/home/petra/czt/parser-zeves/target/test-classes/tests/zeves/instantiateTest.tex.zml
> 	Exception: net.sourceforge.czt.session.CommandException: Key
> (instantiateTest.tex,interface net.sourceforge.czt.z.ast.Spec) not
> computed by net.sourceforge.czt.parser.zeves.ParseUtils@2bccb2
> 	Cause    : null
> Encountered exception during reparsing
> net.sourceforge.czt.session.CommandException
> 
> ... and lots of similar ones.
> <net.sourceforge.czt.parser.zeves.ProofScriptParsingTest.txt><ATT00001..txt><ATT00002..txt>