13.2.6 Verifying

Prev Up Next Page 424 of 800 Search internet

The fourth activity when loading a page is to 'verify' it. 'Verifying' a Logiweb page is a process which takes a Logiweb codex as input and produces a Logiweb codex as output. Verification is a user defined process. See the check page for an example of a user defined proof checker.

If verification finds that the page is correct (contains no formal errors), then it returns the rack of the page unchanged. If verification finds errors in the page, then it hangs an error message on the diagnose hook of the rack.

Unpacking a page may involve loading lots of referenced pages. Referenced pages may contain errors (i.e. have non-empty diagnose aspects). Proof checkers will typically require pages that contain referenced lemmas to be error-free. Logiweb itself does not care whether or not published pages are correct.

Prev Up Next Page 424 of 800 Search logiweb.eu

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