Learn Formatter / format_lean issues

Stream: new members

[Gihan Marasingha]

I've tried and failed to get format_lean or format_project working. It may be because I'm running the exotic operating systems Windows 10 and Mac OS 10.15.

On the Mac, for example, when running format_project, I get the error message

FileNotFoundError: [Errno 2] No such file or directory: PosixPath('/Users/gihan/.elan/toolchains/leanprover-community/lean:3.17.1/bin/lean'):
PosixPath('/Users/gihan/.elan/toolchains/leanprover-community/lean:3.17.1/bin/lean')

The issue seems to be that it has the wrong path. On my system, the correct path should be:

/Users/gihan/.elan/toolchains/leanprover-community-lean-3.17.1

On Windows 10, I also get a FileNotFoundError, though it doesn't specify which file it cannot find.

I receive different error messages when trying format_lean on the file sandwich.lean from the examples folder. On Windows 10, I get Could not resolve host: github.com. On Mac, I get a timeout message:

format_lean.server.LeanError: {'msgs': [{'caption': '', 'file_name': '/Users/gihan/.elan/toolchains/leanprover-community-lean-3.17.1/lib/lean/library/init/data/nat/lemmas.lean',
 'pos_col': 0, 'pos_line': 1127, 'severity': 'error', 'text': '(deterministic) timeout'},
{'caption': '', 'file_name': '/Users/gihan/.elan/toolchains/leanprover-community-lean-3.17.1/lib/lean/library/init/data/nat/lemmas.lean',
'pos_col': 0, 'pos_line': 1141, 'severity': 'error', 'text': '(deterministic) timeout'}], 'response': 'all_messages'}

I'm going to try installing Ubuntu on a virtual machine to see if that works better, but it will take several hours to download over my slow Internet connection.
@Patrick Massot

[Alex J. Best]

This looks like a bug to me, elan toolchains used to have simpler names like 3.4.1 so using the name as the path worked fine. If I explicitly tell it the toolchain format_lean works

format_lean --toolchain="leanprover-community-lean-3.17.1" src/blah.lean

but it seems there is no such option for format_project

[Gihan Marasingha]

Unfortunately, it's only when using format_project that I get this particular error while format_lean gives other errors that aren't resolved with --toolchain. I'll see if I can test format_project on a Lean 3.4.2 project.

[Kevin Buzzard]

This is a single-author project by Patrick Massot, who uses Linux. It's a bit rough round the edges sometimes but @Jason KY. managed to get them working. Jason -- did you use Windows or did you get it working in linux in the end?

[Kevin Buzzard]

I had no problem getting it working in linux.

[Patrick Massot]

This project is currently frozen. It is a prototype that was good enough for my specific goal (producing lecture notes for my lectures). Those lecture notes were using Lean 3.4.2, the last version before the community took over, so I'm not surprised if some stuff is broken now. The plan is to switch to using lean-client-python and integrate format_lean inside leanproject but this has very low priority, so it' won't happen until I start needing it again or someone else does it. I'm sorry, but I simply have too much to do.

[Gihan Marasingha]

Thanks @Patrick Massot . It's working on my Mac with Lean 3.4.2 projects! I'm interested in how it works with a view to translation of Lean code into natural language.

[Jason KY.]

Kevin Buzzard said:

This is a single-author project by Patrick Massot, who uses Linux. It's a bit rough round the edges sometimes but Jason KY. managed to get them working. Jason -- did you use Windows or did you get it working in linux in the end?

Kevin and I were able to get it working on Windows with WSL. But it only formatted one documents before completely bricking! We weren't able to fix it afterwards.

[Utensil Song]

Previously I sent a PR to format_lean to make it work for my scenario (including working partially on Windows without needing WSL) here. Maybe that helps.

I intend to work on merging format_lean into leanproject after I'm done with what's currently on my plate, hopefully soon.

[Utensil Song]

What errors are you getting? ("completely bricking, unable to fix it afterwards.")