lean4lean python script #421
Conversation
|
@pitmonticone : This PR is ready. The scripts work on my local setup. Given the current limitations about toolchain updates in lean4lean, the script will post a message to ping the maintainers and simply not run lean4lean if the toolchains don't match or if lean4lean CLI's build fails for some reason upstream. |
|
awaiting-review |
github-actions
bot
added
the
awaiting-review
|
@euprunin : I took your suggestion here and removed the gitpython dependency completely. Further the script currently performs a best-possible attempt to match lean4lean's toolchain (but does so using lake) with the project toolchain and gracefully exits if this isn't possible. |
|
@pitmonticone : the GitHub clone step fails for want of an ssh key. We need to fix this before any merge. |
|
Sorry but I have not yet found the time to properly review this. Just a quick and trivial question. Why don't we switch the clone URL from SSH to HTTPS as follows? |
|
We could try that. |
|
I'm from mobile now and can't test anything. If you can, let me know if it works. |
|
@digama0 : Is lean4lean expected to be this blazing fast on a project of this size? It seems to be running almost too fast. I'd like to request you to check that I have invoked it correctly in this PR. |
There was a problem hiding this comment.
Was this empty requirements.txt file added unintentionally? If there's no clear reason for its inclusion, you may want to consider removing it.
There was a problem hiding this comment.
My goal is to turn this into a package later. For now it suffices for it to run in CI.
| self.project_name = "equational_theories" | ||
| self.l4l_repo_url = "https://github.com/digama0/lean4lean.git" | ||
| self.toolchain_filename = Path('lean-toolchain') | ||
| self.topPath = Path(os.getcwd()) |
There was a problem hiding this comment.
Since this script deletes subdirectories (using shutil.rmtree), it seems risky to do that in what happens to be the current directory. To avoid any unexpected issues, consider setting a specific working directory.
There was a problem hiding this comment.
This is intentional
There was a problem hiding this comment.
Could you provide more details? What's the reason behind it? Why not fix a working directory to avoid that potential pitfall?
There was a problem hiding this comment.
To use a fresh copy of lean4lean built from lake from scratch. There are good reasons to avoid debugging lake updates when it can be avoided. Git clone reacts poorly with cloning into existing directories. Further a crash can leave lean projects in an inconsistent state. Fresh copies avoid all this fuss.
There was a problem hiding this comment.
I'm not saying you should avoid doing a fresh copy. My suggestion is to perform it in a fixed directory to prevent accidentally deleting files in the user's current working directory.
To clarify:
At the moment, you're essentially running rm -rf lean4lean, without knowing what the current working directory is.
What I'm proposing is a safer approach, like rm -rf [some-fixed-working-directory]/lean4lean.
There was a problem hiding this comment.
People will likely run the scripts in the scripts/ directory locally as well, right? I certainly do.
There was a problem hiding this comment.
The script is meant to be run from the project top level. The most direct use case is the CI. Of course there is a case to be made that the same script can be used as pre-commit or pre-push hooks, we can simply link to the script from bash.
There was a problem hiding this comment.
For locally running this script I can include an instruction that says it should be run from the top level. For the moment I am prioritising the CI, where we can't necessarily pin the project path better than getcwd(). I do agree an absolute path would be ideal.
There was a problem hiding this comment.
I'm not advocating for hard coding an absolute path. Instead, I recommend using __file__ to obtain the script's location and then constructing the appropriate working directory relative to it.
There was a problem hiding this comment.
This is a good idea.
EDIT: One issue is it fixes the subdirectory of the script and makes it fragile for use in other projects
Add a lean4lean verification script