Zulip Chat Archive

Stream: lean4

Topic: lake script API

Arthur Paulino (Jun 26 2022 at 11:00):

Hi!
Looking at the lake script API, I feel like lake script run foo is rather long/verbose. So I thought of having lake script foo again (like we had before) and lake scripts as the call to list available scripts and their docstrings in a single command.

I also think that having all scripts in the lakefile.lean file can become a bit crowded, so my other idea is being able to implement scripts in their own files, which can be located in a customizable folder (default = scripts). Or, heck, being able to link to scripts from other repositories would be cool too :D

What do you guys think?

Gabriel Ebner (Jun 26 2022 at 12:05):

See also https://github.com/leanprover/lake/issues/82

Tomas Skrivan (Jun 27 2022 at 08:39):

What is the reason for not having lake run foo? It is the shortest and most clear. I'm constantly getting the order of script and run incorrectly.

Arthur Paulino (Jun 27 2022 at 10:26):

lake script has other options like doc foo and list iirc. But both of those can be tackled by a lake scripts at the same time. I don't think it's worth making the command to run scripts longer because of secondary options, especially because they are not used very often (I never used them)

Mac (Jun 27 2022 at 18:59):

@Arthur Paulino Feel free to post an issue with the request on the Lake repo. That way you can know when I have completed it. :)

Arthur Paulino (Jun 27 2022 at 19:21):

https://github.com/leanprover/lake/issues/88 :+1:

Arthur Paulino (Jun 27 2022 at 19:22):

I left the scripts folder out because there might be some unnecessary complications when dealing with scripts that have repeated names

Mac (Jun 27 2022 at 20:27):

@Arthur Paulino That issue made me realize that your suggestion was actually slightly different than @Tomas Skrivan's (sorry for my mistaken quick skim). Primarily this part:

  • Resurrect the old lake script foo as the command to run the script foo

The old command was lake run foo, which I would be happy to resurrect as an abbreviation for lake script run. I would also be willing to add a lake scripts as an abbreviation for lake script list. However, I do want to keep more granular lake script <subcommand> around as an option.

How does that sound?

Arthur Paulino (Jun 27 2022 at 20:29):

That's even better since run is shorter than script

Last updated: Dec 20 2023 at 11:08 UTC