leanprover-community / mathport

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

Too Hard to use for me. #258

Closed chenjulang closed 3 months ago

chenjulang commented 3 months ago

Can we have a online version? Input a lean3 project, Output a lean4 project.

digama0 commented 3 months ago

Sorry, mathport is nearing EOL and is not likely to get such a makeover any time soon. You should try to follow the instructions and ask on https://leanprover.zulipchat.com/ if you get stuck.