Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
Continuation of #1311. It turns out that there were indeed some issues in the original implementation: specifically, because the zero scanning was happening after QuoteFilter ran, it would sometimes buffer up pieces of the input stream, which are lost when doing the lexer hard reset used in this code. The fix is to instead instrument the input to the lexer so that it can't see any more of the input than we allow it to.
I also added some tests per the request at #1311, including one that detects the issue this PR fixes.
mn200
commented
1 month ago
Continuation of #1311. It turns out that there were indeed some issues in the original implementation: specifically, because the zero scanning was happening after QuoteFilter ran, it would sometimes buffer up pieces of the input stream, which are lost when doing the lexer hard reset used in this code. The fix is to instead instrument the input to the lexer so that it can't see any more of the input than we allow it to.
I also added some tests per the request at #1311, including one that detects the issue this PR fixes.