House keeping: tidying everything

[oliver-butterley]

• Split lean code into separate files
• Streamline github action
• Add vscode nice settings
• Bump lean version and make required correction to one proof
• Etc

[oliver-butterley]

I suggest the "Squash and merge" commit method to reduce the main history.

[mseri]

Nice! Thanks. As per the merge: Do we really care about having a such a concise history when your commits are already so explicative? I’d be actually inclined in merging with a merge commit

[oliver-butterley]

I feel we are saying the same thing but with different words... Most importantly, I don't have a strong point of view on this, this is a minor preference I have.
With a squash and merge the PR commits are squashed into a single commit. Instead of seeing all of a contributor's individual commits from a topic branch, the commits are combined into one commit and merged into main.
This has the benefit of keeping the commit history in the main repo a bit cleaner. With a normal merge all the commits from the PR are added to the commit history.

[mseri]

Yes I know the difference, I meant that I in general like to see the breakdown of the history :) I tend to use squash and merge only when the PR is messy

[mseri]

I assume the license is apache to fit in with lean/mathlib one

[oliver-butterley]

I assume the license is apache to fit in with lean/mathlib one

Yes, licence is there apache license, identical to mathlib. I don't want to ever think about legal things but I understand that such is useful to guarantee the code is a always free in the future.

[oliver-butterley]

Yes I know the difference, I meant that I in general like to see the breakdown of the history :) I tend to use squash and merge only when the PR is messy

Yes, actually that makes good sense.