Bug with self-inclusion (with probably easy fix)

[benjub]

If you try to MM> read test.mm where test.mm contains $[ test.mm $], this raises "BUG 1765" instead of simply ignoring that inclusion statement as a recursive one.
I found this while fixing the same bug in https://github.com/benjub/mmverify.py/blob/faster/mmverify.py. A straightforward fix there: when creating the "input stream", add the current file to the set of already read files (see the line self.imported_files = set({pathlib.Path(file.name).resolve()}), which works with the later line if file not in self.imported_files:...). A similar fix should be doable in metamath.c.

[digama0]

I think this should be rejected. Cyclic inclusion patterns should always be rejected because they have unclear ordering.

[benjub]

Rejecting cyclic inclusions is reasonable. But the fix would be less straightforward, it seems, since the program should detect cycles ?

[david-a-wheeler]

It shouldn't be an error, it should just be ignored.

Metmath book section 4.1.2 "Preprocessing" (page 113) has the spec:

"A file self-reference is ignored, as is any reference to the top-level file (to avoid loops)".

This is easily addressed; every time an inclusion is seen, you ignore it if that file has already been requested, otherwise add that file to the list of files that have been requested. The key is that the initial load of the file needs to add that filename to the list of files being requested.

[benjub]

This is easily addressed; every time an inclusion is seen, you ignore it if that file has already been requested, otherwise add that file to the list of files that have been requested. The key is that the initial load of the file needs to add that filename to the list of files being requested.

Yes, that is exactly the fix that I mentioned above and that I implemented in my "faster" branch of mmverify.py mentioned above.

[digama0]

If this is already in the spec, then so be it. As an aside, file self references and references to the top level file are not sufficient to avoid loops: If A -> B -> C -> B then no file is self-referential or references A but there is still an import cycle.

[david-a-wheeler]

Yes, we agree that asserted cycles can be indirect.

I believe the intent for processing A -> B -> C -> B ( where -> is "imports") was to do this: Load A, load B, load C, ignore second request to B. So the solution to counter cycles was to unroll the imports & ignore anything that would refer to something already important "previously".