aniva/Pantograph

Mathlib4 Parsing Error #122

New issue

Closed

opened 2024-11-15 23:11:50 -08:00 by aniva · 0 comments

aniva commented

2024-11-15 23:11:50 -08:00

Owner

https://github.com/lenianiva/PyPantograph/issues/44

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

The error occurs when parsing Mathlib/ModelTheory/Syntax.lean

https://github.com/lenianiva/PyPantograph/issues/44 ``` File "<...>/PyPantograph/pantograph/server.py", line 244, in tactic_invocations raise ServerError(result["desc"]) pantograph.server.ServerError: unknown constant 'term.pseudo.antiquot' ``` The error occurs when parsing `Mathlib/ModelTheory/Syntax.lean`

aniva added this to the v0.3 milestone

2024-11-15 23:11:50 -08:00

aniva added the

labels

2024-11-15 23:11:50 -08:00

aniva self-assigned this

2024-11-15 23:11:50 -08:00

aniva modified the milestone from v0.3 to v0.2.22

2024-12-06 00:09:29 -08:00

aniva referenced this issue from a pull request that will close it,

2024-12-09 21:40:36 -08:00

feat: Extract type error and new constants #128

aniva added a new dependency

2024-12-09 21:43:23 -08:00

#128 feat: Extract type error and new constants

aniva closed this issue

2024-12-11 01:25:36 -08:00

Sign in to join this conversation.

No labels

part/Environment

pending-measurement

No milestone

No project

No assignees

1 participant

Notifications

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Depends on

#128 feat: Extract type error and new constants

aniva/Pantograph

Reference: aniva/Pantograph#122

No description provided.