Setup Test and CI

[utensil]

This PR adds basic tests and CI for format_lean. This PR is submitted for the initial review and discussions.

Rationale: I need to make modifications and add features to this tool at least for myself, but before adding anything serious, it's better to set up some basic tests and CI.

Details:

• For CLI, I switched from scripts to entry_points for
  • Windows friendly: the scripts way doesn't work on Windows, Windows expects an .exe instead of a file without extension. This would be properly handled by entry_points.
  • test friendly: the main implementations of CLI was under bin, so the test can't import them and run tests on them, by moving them back to the main source, they can be accessed
• I removed the extra src directory layer so it follows the standard directory structure that pytest would expect, this might be controversial, but I don't know how to make pytest recognize the extra src and don't want to do extra configuration since "conversion over configuration" would save much trouble
• I added missing dependencies that would not be noticed on a local machine full of python packages
• I updated the lean version and mathlib version and everything seems to be working
• I used a fork of mathlibtools of my own (will submit PR soon) to fix Support looking for leanpkg.toml in cwd mathlib-tools#59 in order for the CI to pass

P.S. Sorry for the small commits (which is to keep every commit self-explanatory and easy to review), but it can be squashed when merging anyway.

[PatrickMassot]

Thank you very much for trying to contribute to format_lean! But you should have discussed before working.

The grand plan is to merge format_lean into leanproject, and use lean-client-python. In particular I want to officially remove support for converting files that are not part of a project (which correspond to the format_lean script, as opposed to format_project).

I have way too many projects going on in parallel, and format_lean has very low priority since the current version already fulfill my needs and, as far as I know, nobody else uses it. But if you have time and motivation to work on this project, this is the path we want to follow (I can give more details if you intend to work on this).

Also note that pytest has no trouble adapting to any file layout, but this is besides the point.

[utensil]

Thank you for your time!

But you should have discussed before working.

Sorry, will do. Basically I was trying to make it "work" locally and the whole CI/PR thing is a side effect. Sending the PR simply because my local modification has reached a point that I need to check the compatibility with the original plan on format_lean.

The grand plan is to merge format_lean into leanproject, and use lean-client-python. In particular I want to officially remove support for converting files that are not part of a project (which correspond to the format_lean script, as opposed to format_project).

Great! Then my efforts will be redirected to that. P.S. format_project is better to be a subcommand instead of a global CLI (the naming is not scoped) anyway. Merging into leanproject will do that.

But if you have time and motivation to work on this project, this is the path we want to follow (I can give more details if you intend to work on this).

I do have some motivations for it as a side project and some time too(but no promise on that because I have a heavy day job completely unrelated to math or lean). I'll get back on Zulip to discuss it further after I learn more about leanproject and lean-client-python, i.e. reading their source.

[utensil]

Closing as this PR is obsolete.