sorear / smetamath-rs

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

Should we remove the hybrid mode from database parsing? #18

Open sorear opened 8 years ago

sorear commented 8 years ago

The database parse method takes a file name, and a file name/content association. You can parse data in memory by passing an association list, or you can parse a file on disk by not passing the association.

Currently, if you pass an association but there are $[ $] references to names that don't hit, it will fall back to fetching those files from disk, so you can parse data from a combination of disk and program memory. This feature was not implemented on purpose and I'm not sure it's useful.

@digama0 it occurs to me that, deliberate or not, this might be useful for IDE integration and should be kept on that account?

digama0 commented 8 years ago

I don't get it. How does it know what files to populate the association with before it has read the $[ $] command?

By IDE integration, do you mean that the user has added a new $[ $] reference to an unknown file in incremental mode? Ideally there should be no difference between the success of one-shot verification vs incremental mode, which means anticipating the addition of new files as well. Unless I'm misunderstanding your question...

sorear commented 8 years ago

The idea is that you'd pass the association if you 1. already known what files will be needed, and 2. don't want it to hit disk. That's a feature copied from SMM2, where it basically existed to make the test suite work. So we'll need some version of it for #1. Now consider what will happen when I try to write a test for "what error is generated when an included file can't be found"…

digama0 commented 8 years ago

I would suggest keeping this hybrid behavior, but add a flag to disable the disk read fallback for test mode. That should cover your bases.