search

metamath / metamath-knife

Metamath-knife can rapidly verify Metamath proofs, providing strong confidence that the proofs are correct.
Apache License 2.0
26 stars 11 forks source link

Crash in case of ambiguous grammar #52

Open tirix opened 2 years ago

tirix commented 2 years ago

See set.mm PR#2379: In case of an ambiguous grammar ($a class A B : $.), the program panics:

> cargo run -- -g -p ../set.mm/set.mm 
thread 'main' panicked at 'called `Option::unwrap()` on a `None` value', src/grammar.rs:1161:73
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
thread 'main' panicked at 'called `Result::unwrap()` on an `Err` value: Any { .. }', src/database.rs:292:31

It shall rather issue a diagnostic complaining about the grammar being ambiguous.