Error with custom notation

lecopivo commented 2 years ago

Description

Defining a simple notation

prefix:max "■" => Nat.succ

produces an error

Error: unknown constant 'Lean.Syntax.Preresolved.decl'

Reproducing the issue

Lean file leanink_fail.lean:

prefix:max "■" => Nat.succ

#eval ■ 1

Run leanInk analyze leanink_fail.lean, the resulting leanink_fail.lean.leanInk is:

[{"messages":[{"contents":"Error: unknown constant 'Lean.Syntax.Preresolved.decl'","_type":"message"},{"contents":"Error: unknown constant 'Lean.Syntax.Preresolved.namespace'","_type":"message"}],"goals":[],"contents":"prefix:max \"■\" => Nat.succ","_type":"sentence"},{"contents":"\n\n#eval ","_type":"text"},{"messages":[{"contents":"Error: elaboration function for '«term■_»' has not been implemented\n  ■1","_type":"message"}],"goals":[],"contents":"■ 1","_type":"sentence"},{"contents":"\n","_type":"text"}]

Environment information

Operating System: Ubuntu 20.04 LeanInk version: 037440a09fbd321ea6bdf9c8001b64ed122060e0

Kha commented 2 years ago

You need to build LeanInk against the same Lean version as lean --version reports in this project/directory

lecopivo commented 2 years ago

Ahh my default lean version is version 4.0.0-nightly-2022-08-20 and LeanInk in that commit uses 08-22

lecopivo commented 2 years ago

Would be nice if LeanInk would warn about this. That the current lean version is not matching the version you build LeanInk with.

Also if LeanInk is so fussy about the version, then the installation instruction with

sh -c "$(curl https://raw.githubusercontent.com/leanprover/LeanInk/main/init.sh -sSf)"

is pretty much useless. (Well the command didn't work for me anyway)

Kha commented 2 years ago

leanprover / LeanInk