write_stmt_use in axiom_use.rs hates uncompressed proofs.

[arpie-steele]

This is two problems: the loop statement runs out-of-bounds and always starts with i = 1 . The canonical test is set.mm/miu.mm which has both zero-length wffs and a single uncompressed proof at the end of the file where out-of-bounds errors hit the EOF.

If you had code like:

impl StatementRef<'_> {
    /// Iterates over explicit label content of proof.
    /// Implicit references to floating and essential hypotheses are ignored.
    /// Uncompressed proofs will often reference the same label multiple times.
    pub fn for_proof_statement_labels(&self, mut per_label: impl FnMut(&[u8])) {
        let len = self.proof_len();
        if len <= 0 {
            return;
        }
        let token = self.proof_slice_at(0);
        if token == b"(" {
            // Compressed proof has label-containing preamble between parentheses
            for index in 1..len {
                let token = self.proof_slice_at(index);
                if token == b")" {
                    break;
                }
                per_label(token);
            }
            return;
        }
        // Uncompressed proof is nothing but statement-labels
        per_label(token);
        for index in 1..len {
            per_label(self.proof_slice_at(index))
        }
    }
}

Then you could replace this code which assumes compressed proofs:

                    let mut i = 1;
                    loop {
                        let tk = sref.proof_slice_at(i);
                        i += 1;
                        if tk == b")" {
                            break;
                        }
                        if let Some(usage2) = stmt_use_map.get(tk) {
                            usage |= usage2
                        }
                    }

with:

                    sref.for_proof_statement_labels(|tk| {
                        if let Some(usage2) = stmt_use_map.get(tk) {
                            usage |= usage2
                        }
                    });

[digama0]

write_stmt_use in axiom_use.rs hates uncompressed proofs

Yes. What is the motivation for supporting uncompressed proofs in axiom_use?

[arpie-steele]

write_stmt_use in axiom_use.rs hates uncompressed proofs

Yes. What is the motivation for supporting uncompressed proofs in axiom_use?

The promise in metamath-rs/README.md that the library "supports all Metamath proof formats. In particular, Metamath-knife adds support for all Metamath proof formats (uncompressed, compressed, package, or explicit.

[digama0]

The suggestion is not enough to support all proof formats. But my question remains: why do you need this? Is it just a feeling of incompleteness?

[arpie-steele]

Short story, yes. Specifically, the published 3.8 library seems incomplete with respect to its advertised functionality.

I was going to re-implement a tool which generalizes condensed detachment (letting any statement with essential hypotheses fill in for ax-mp) and I wanted to use set.mm/miu.mm (featured in the Metamath book, Appendix D) as a test case, which famously has an uncompressed proof so that one might follow along with its use of a syntax axiom (we) which renders sequences of 0 tokens as legal wffs.

I thought condensed detachment might make.for a nice playground was was planning to build on the metamath-rs library and eventually implement a browser-based workspace. That line I quoted above showed up on "crates.io" which is why I started looking into not writing all the database-handling code myself.

So I was still exploring the code to decide if I want to use it as-is or as some sort of hard-to-maintain fork when the metamath-knife crashed in the code common to --stmt-use or -X when I tried those with miu.mm. (Also -E doesn't seem to represent we in its diagram, but I'm not sure if that is a known issue, still under development, or working as designed. The non-syntax axioms from miu.mm get left as unconnected nodes, which I suspect is because their labels begin with neither ax- nor df-)