sorear / smetamath-rs

sorear's Metamath system engine - version 3 Rust
Apache License 2.0
22 stars 6 forks source link

parallel parsing mishandles repeated includes #22

Open sorear opened 8 years ago

sorear commented 8 years ago
$$ target/release/smetamath --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 smetamath3 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.