Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Parsing error using |x| local notation in calc tactic #17

Open
jasonrute opened this issue Jul 1, 2021 · 0 comments
Open

Parsing error using |x| local notation in calc tactic #17

jasonrute opened this issue Jul 1, 2021 · 0 comments

Comments

@jasonrute
Copy link
Owner

jasonrute commented Jul 1, 2021

Currently, we get the following error when trying to process the data for bernstein.lean.

data_mathlib/lean_files/mathlib/src/analysis/special_functions/bernstein.lean
Traceback (most recent call last):
  File "/root/code/formal/formal/lean/lean_proof_recording/lean_proof_recording/pipeline/extract_proof_data.py", line 487, in run
    parser_ast = parser.read_begin()
  File "/root/code/formal/formal/lean/lean_proof_recording/lean_proof_recording/parser.py", line 1108, in read_begin
    tactics = self.read_tactic_list()
  File "/root/code/formal/formal/lean/lean_proof_recording/lean_proof_recording/parser.py", line 1040, in read_tactic_list
    self.raise_error(f'Expected "," or "{right}"')
  File "/root/code/formal/formal/lean/lean_proof_recording/lean_proof_recording/parser.py", line 384, in raise_error
    raise Exception(f"{msg}:\n{self.format_file_location()}")
Exception: Expected "," or "end":
data_mathlib/lean_files/mathlib/src/analysis/special_functions/bernstein.lean:240:5
0239:     |(bernstein_approximation n f - f) x|
          ^

The issue, is two fold:

  • There is a local notation in the file using |, which is normally used to delimit cases in a match or in an inductively defined term proof.
  • It is used inside calc which is one of the few cases where we have no information from Lean on how to parse, so I have to just scan along until we reach a reasonable end point. Currently that is set as one of "end", ";", ",", "|", "<|>", a right bracket, or a user command (but taking nesting parentheses and match statements into account).

Hence it is done scanning too early on the calc tactic. Luckily this is caught as an error, since the calc tactic is inside a tactic list so we know that the calc tactic can actually only end with "," or "end" (or ";", or "<|>", if it was inside a semicolon list or alternative inside that outer tactic list.)

I see two solutions:

  1. Scan the calc tactic in stages. Since the calc tactic is of the form calc xxx : xxx ... xxx : xxx ... xxx : xxx (where the xxx are terms), I could first scan until :, and then scan until ... or one of the end delimiters. In this particular case, that should catch the user notation since it is always on the left of the :.
  2. Make the end points for scanning the calc tactic depend on if I am inside a tactic list or a by.

I think I like option (1) better, but let me think about it for a bit first.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant