Axiom usage verification

[tirix]

Naive but functional axiom usage check.

Introduces a -u option which checks that $j usage 'xxx' avoids 'yyy' commands are respected.

This only checks axioms dependencies, not all statements. Currently issues an "Unknown label" diagnostic if the axiom declared as avoided actually only declared further down in the database. This is the simpler implementation, but this generates many warnings with the current set.mm.

[jkingdon]

Oh nice. I started looking into this but realized I would face a pretty steep/long learning curve in terms of how to even Rust.

This only checks axioms dependencies, not all statements.

Is relaxing this as simple as removing the label.starts_with(b"ax-") check? Not that I tried measuring the memory use without and without that or anything. I guess we can live with doing it only for axioms, though. Certainly that's our main use case.

Currently issues an "Unknown label" diagnostic if the axiom declared as avoided actually only declared further down in the database. This is the simpler implementation, but this generates many warnings with the current set.mm.

I suppose the cheesiest way out is to just silently skip any unknown labels. I mean that is technically correct in the sense that a proof does indeed avoid all usages of statements defined later. And we could always do something fancier later.

Is it too much scope creep to ask for a unit test or two? They seem to be easy to write based on examples like https://github.com/david-a-wheeler/metamath-knife/blob/4c4e873954b7121e74c74e819abb076cc91df299/src/formula_tests.rs#L48 and I'm especially thinking of a test for the case(s) that violations of $j usage are indeed detected (tests that acceptable usages produce no errors would be fine but are less vital in the sense that just running this check on set.mm would get us that).

[tirix]

Currently issues an "Unknown label" diagnostic if the axiom declared as avoided actually only declared further down in the database. This is the simpler implementation, but this generates many warnings with the current set.mm.

I suppose the cheesiest way out is to just silently skip any unknown labels.

Yes, I did just that in the last commit. This way no error remains with the current set.mm database.

This only checks axioms dependencies, not all statements.

Is relaxing this as simple as removing the label.starts_with(b"ax-") check?

That would not be sufficient: that test is only making the difference between definitions (df-) and actual axioms (ax-) for axiom statements ($a -- StatementType::Axiom). You'd need to also to cover provable statements ($p -- StatementType::Provable), which is currently another match branch. That would certainly use up way more memory, so I kept it like this in the latest commit.

Is it too much scope creep to ask for a unit test or two?

Certainly not! I've added a test in the last commit, generating that "Usage Violation" error.

[jkingdon]

I was unable to get any failed checks.

I checked out the branch, ran cargo build --release, modified set.mm to add

$( $j usage 'ac9' avoids 'ax-inf' 'ax-inf2' 'ax-ac' 'ax-ac2' 'ax-3' 'ax-1'; $)

after ac9, and then ran target/release/metamath-knife --verify-usage ~/work/set.mm/set.mm. I got output ending in 0 diagnostics issued.

As far as I could tell this had something to do with how the diagnostics propagate up from UsagePass to the reporting of results, but I suppose it is possible I am seeing something strange which others are not.

[tirix]

I got output ending in 0 diagnostics issued.

After a quick check I see that:

• when I put the $j command inside of the ac9 block, no diagnostic is issued,
• when I put the $j outside the block, at the top level, the diagnostics are correctly issued.

[jkingdon]

I got output ending in 0 diagnostics issued.

After a quick check I see that:

* when I put the `$j` command inside of the `ac9` block, no diagnostic is issued,

* when I put the `$j` outside the block, at the top level, the diagnostics are correctly issued.

Ooh, nice observation.

I can reproduce this problem by adding the enclosed test to usage_tests.rs.

Seems like existing practice is that $j is legit inside ${ (I see an existing example using $j congruence from before we started doing any of this $j usage stuff).

#[test]
fn nested() {
    let mut db = mkdb(b"
$c wff |- > $.  $v a $.
wa $f |- a $.
ax-1 $a |- > a $.

${
  thm1 $p |- > a $= wa ax-1 $.
  $( $j usage 'thm1' avoids 'ax-1'; $)
$}
");
    assert_eq!(db.parse_result().parse_diagnostics(), vec![]);
    let usage = db.verify_usage_pass();
    let diags = usage.diagnostics();

    assert_eq!(diags.len(), 1);
    assert_matches!(diags[0], (_, UsageViolation(..)));
}

[digama0]

Seems like existing practice is that $j is legit inside ${ (I see an existing example using $j congruence from before we started doing any of this $j usage stuff).

Yes, you can put $j anywhere at statement level. Some $j commands could even make use of the scope for something, although to my knowledge none do.

[tirix]

Seems like existing practice is that $j is legit inside ${ (I see an existing example using $j congruence from before we started doing any of this $j usage stuff).

Yes, you can put $j anywhere at statement level.

It turns out that the parser's collect_definitions function only handled top-level $j commands. The last commit corrects that behaviour. This will also benefit other users of $j commands.

Note that typesetting comments are also only treated when at top-level. I have not changed that behaviour.