search

metamath / metamath-knife

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

parallel parsing mishandles repeated includes #81

Open tirix opened 2 years ago

tirix commented 2 years ago

From SMM3 issue #22

$$ target/release/metamath-knife --text A '$[ B $] $[ C $]' \
    --text B '$[ C $] $c X $.' --text C '$c X $.'
C:3-4:Error:This symbol is already active in this scope
B:11-12:Note:Symbol was previously declared here

A starts by including B which starts by including C, so C's version of X should be the logically first one, but metamath-knife gets confused during readahead and decides that the "real" include of C is the one in A, messing up the order. The included check in read_and_parse is misplaced, not sure right now where it belongs.