Server Error when running frontend.process on mathlib4

[sorgfresser]

I successfully built mathlib4, started the PyPantograph server on it and ran tactic invocations on the file Mathlib/ModelTheory/Syntax.lean. This resulted in

  File "<...>/PyPantograph/pantograph/server.py", line 244, in tactic_invocations
    raise ServerError(result["desc"])
pantograph.server.ServerError: unknown constant 'term.pseudo.antiquot'

This is especially interesting because the term in question is not even mentioned in the whole file.

[lenianiva]

What version of mathlib are you using?

Mathlib4 seem to have this issue internally: https://github.com/leanprover-community/mathlib4/blob/2e8dbf68904ffbccb7529f87a2207d6289e6a2e7/Mathlib/Data/Nat/Digits.lean#L812

[sorgfresser]

My version is new enough to suffer from this, I'll try downgrading and report back!

[lenianiva]

My version is new enough to suffer from this, I'll try downgrading and report back!

Can you use the v4.12 tag of mathlib?

[sorgfresser]

Facing the same error on tag v4.12 upon running frontend.process on file mathlib/Mathlib/ModelTheory/Syntax.lean

[lenianiva]

Fixed in upstream: https://git.leni.sh/aniva/Pantograph/pulls/128. Will merge by the end of the week.

You can try running this in repl by

lake env ~/Projects/atp/Pantograph/.lake/build/bin/repl Mathlib < /tmp/target.jsonl

where target.jsonl is

frontend.process {"fileName": "Mathlib/ModelTheory/Syntax.lean", "invocations": true, "sorrys": false, "newConstants": false}

[lenianiva]

This PR helped me and others track down another bug in Lean 4: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/What.20is.20.60term.2Epseudo.2Eantiquot.60.3F/near/487319979

[sorgfresser]

Awesome, thanks!

This PR helped me and others track down another bug in Lean 4: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/What.20is.20.60term.2Epseudo.2Eantiquot.60.3F/near/487319979
I was wondering what exactly happened, interesting to see it is actually related to Lean.