Error with custom notation

[lecopivo]

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]

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

[lecopivo]

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

[lecopivo]

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]

Yeah, see also #21 (comment)