14.245 The location of errors in proofs

Prev Up Next Page 716 of 800 Search internet

Errors in proofs may be particularly difficult to locate. That is because a proof undergoes the following to be verified:

First, the proof is macro expanded and stored in the codex. Typography, among other, is lost during macro expansion.

Second, the proof is 'tactic expanded'. The output of tactic expansion is a low level proof expressed in the Logiweb sequent calculus. Line numbers in proofs, among other, is lost during tactic expansion.

Third and finally, the low level proof is verified.

Macro expansion and tactic expansion are equally powerful, and it is up to the designer of macros and tactics to decide what should occur when. A difference between the two is that the output of macro expansion is stored in the codex. For that reason, the output of macro expansion is kept in memory. Furthermore, the output of macro expansion is stored in the rack file when a page is dumped to cache. In contrast, the output of tactic expansion is fed to the verifier and is then discarded. For that reason, the output of tactic expansion does not take up any resources once a page is verified.

Errors may be found during tactic expansion and during verification. In both cases, the proof may have undergone arbitrary transformations during macro expansion and thus location of errors is non-trivial.

Tactic expansion and verification works on parse trees which originate from macro expansion. Provided the macros are expressed correctly, those parse trees contain debug information which indicates where the parse trees came from in the body of the tree. When an error occurs during tactic expansion or verification, the error message generator uses this information to locate the error in the body of the page, i.e. in the page before macro expansion. Once this is done, the error message generator tries to find a description of that location such as 'Line L10 in the proof of Lemma 7.2.1'.

It could be nice if the error message generator could go one step further and tell which line of the lgs source was in error. The error message generator itself cannot do it because it does not (and should not) have access to the lgs source. The lgc compiler would be able to locate errors in the lgs source being translated, which constitutes a nice to have facility which might emerge in the future.

For referenced pages the lgs source may no longer exist. Locating errors to lgs sources only makes sense for the lgs source being translated.

Prev Up Next Page 716 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05