search

leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4
Apache License 2.0
40 stars 15 forks source link

Mathport crashes on the latest mathlib4 #228

Closed eric-wieser closed 1 year ago

eric-wieser commented 1 year ago

The mathport CI is giving the error

Failed to port { package := "Mathbin", mod3 := `ring_theory.subring.basic }

The error message comes from

https://github.com/leanprover-community/mathport/blob/98107af65ef2cf6dd59c0bc1d062e65f1a430514/MathportApp.lean#L22

Is there stderr or stdout from the process that we could propagate which might contain a better message?

Zulip

gebner commented 1 year ago

Fixed by b515f2fb449110ef1010041691f43437c05ebd34