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

File inclusion outside of top level #90

Closed tirix closed 2 years ago

tirix commented 2 years ago

One of the optimisations making metamath-knife fast is to use multi-threading. This means that databases are split into segments, and each segment is then handled completely separately, in a different thread.

The segments themselves are chosen to be at the start of main chapters, and at file inclusions. In order to allow this, a note in parser.rs mentions:

We require file inclusions to be between statements at the top nesting level (this has been approved by Norman Megill).

That requirement is also stated in the Metamath Book, chapter 4.1.2, but depending on the discussion in Metamath.exe#85, we might prefer to allow file inclusion outside of the top level.

I'm opening this issue to discuss how this limitation could be removed. It might be possible to allow file inclusion at any position outside of other statements, so that placing a file inclusion outside of the top level would only mean that metamath-knife would not be optimally efficient.

The UnclosedBeforeInclude would need to be changed into a warning that parsing is not optimal.

digama0 commented 2 years ago

Independently of implementation issues, I think it is bad design-wise to have inclusions not at the top level, because then it means that things in the included file that appear to be at the top level are not actually at the top level, which makes it harder to understand scoping across files. I have never heard of a programming language which allows that sort of thing.

tirix commented 2 years ago

Two examples I can immediately think of are C and PHP:

If the include occurs inside a function within the calling file, then all of the code contained in the called file will behave as though it had been defined inside that function. So, it will follow the variable scope of that function.

Both allow it technically, but I think anyone would argue it's really bad. I'll close this issue for now.

digama0 commented 2 years ago

Yeah, I was tactfully avoiding mentioning the C include behavior, which is lexer level similar to metamath.c's implementation and so lets you do some horrible horrible things like includes in string constants...

I think it is generally a side effect of very dynamic languages that just implement it "operationally" and don't think too hard about the meaning of the construct in terms of declarative code structuring.