Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: add a step that logs the version of lake and lean #24

Merged
merged 9 commits into from
May 19, 2024

Conversation

oliver-butterley
Copy link
Contributor

Add a step to the action which:

  • reports if mathlib is used
  • reports the lake version
  • reports the lean version

resolves #12

@oliver-butterley
Copy link
Contributor Author

Give me some feedback about precisely what behaviour is required and I can modify this.

  • Current output is as seen in attached images.
  • Since this is the first time that lake and lean are used it also shows them being obtained by elan. T
  • Concerning the mathlib check, there are three options: true, false, not checked. In order to get the tested for and false option the corresponding sh file was modified.
  • In the case of mathlib dependency not being checked, currently displays "" but could be modified to be more communicative if required. Alternatively always run the mathlib check, whatever the setting of mathlib-cache. (And hopefully the lake CLI is improved soon and there is more elegance to accessing the lean project info.)

no check mathlib
no mathlib
with mathlib

@austinletson
Copy link
Collaborator

This PR looks great! This will allow existing projects such as import-graph to simplify their workflow even more by using lean-action.

I have a suggestion that might improve the user experience, though it deviates slightly from the original issue. Since some Lean setup happens during lean --version/lake --version, should we incorporate this logging into the install elan step, perhaps renaming it to setup lean? This would:

  • Contain any Lean installation issues within the setup lean step, making troubleshooting easier.
  • Provide users who don't need version details a cleaner workflow.

If we decide to go this route, we could potentially omit the Mathlib check logging since the detect Mathlib step already covers it.

Let me know what you think!

@oliver-butterley
Copy link
Contributor Author

I like your plan, simplicity is a good thing.

@oliver-butterley
Copy link
Contributor Author

😱 I'm sorry! I'm perfectly aware of this issue with the paths in gh actions and I also thought I was testing each thing I did before opening the PR. However it appears that I wasn't capable of anything sensible late on Friday after a long week. I'll mend it carefully soon. Probably simplest to just add the paths to each command, e.g., .elan/bin/lean --version.

@oliver-butterley
Copy link
Contributor Author

I've updated these two lines to log the version. I tested it on a test repo and it does as expected.

@austinletson
Copy link
Collaborator

Looks great. Thanks @oliver-butterley!

@austinletson austinletson merged commit ae16192 into leanprover:main May 19, 2024
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Enhance version information logging
2 participants