Changes in the parser

Stream: metaprogramming / tactics

[Leni Aniva]

I have this code which worked for an earlier version of Lean but does not work in 4.19 anymore. I could not find a relevant change in the changelog:

import Lean
open Lean

def fileName := "<example>"

def main := do
  let env: Environment ← importModules
    (imports := #[`Init])
    (opts := {})
    (trustLevel := 1)
  let syn? := Parser.runParserCategory
    (env := env)
    (catName := `term)
    (input := "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))")
    (fileName := fileName)
  match syn? with
  | .ok syn => IO.println s!"{syn}"
  | .error e => IO.println s!"{e}"

The error is

<example>:1:23: expected token

What has changed? This is fine

#check ∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))

[Justin Asher]

What version did it work with?

[Leni Aniva]

4.18

[Damiano Testa]

Does it work if you do not use the notation for or?

[Jannis Limperg]

I believe importModules got a new argument loadExtsthat is false by default, but needs to be true to load env extensions.

[Justin Asher]

import Lean
open Lean

def fileName := "<example>"

def main := do
  let env: Environment ← importModules
    (imports := #[`Init])
    (opts := {})
    (trustLevel := 1)
    (loadExts := true)
  let syn? := Parser.runParserCategory
    (env := env)
    (catName := `term)
    (input := "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))")
    (fileName := fileName)
  match syn? with
  | .ok syn => IO.println s!"{syn}"
  | .error e => IO.println s!"{e}"

Yep. Here is the relevant commit.

[Auguste Poiroux]

There was the same issue when updating the REPL from v4.18.0 to v4.19.0-rc2. Setting loadExts := true solved it: PR, #Machine Learning for Theorem Proving > request for help on the REPL @ 💬