Skip to content
This repository has been archived by the owner on Oct 25, 2023. It is now read-only.

Simplify API to run scripts #88

Closed
arthurpaulino opened this issue Jun 27, 2022 · 1 comment
Closed

Simplify API to run scripts #88

arthurpaulino opened this issue Jun 27, 2022 · 1 comment
Labels
enhancement New feature or request
Milestone
v3.2.2

Comments

@arthurpaulino
Copy link
Contributor

The current command to run Lake scripts has the keyword run, which looks a bit too verbose (and can be confusing, even).

Suggestion:

  • Resurrect the old lake script foo as the command to run the script foo
  • Add a lake scripts as the command to list available scripts and their docstrings

Zulip thread
@tydeu tydeu added the enhancement New feature or request label Jun 28, 2022
@arthurpaulino
Copy link
Contributor Author

After some discussion, a lake run ... as a shortcut for lake script run ... should be enough.

@tydeu tydeu added this to the v3.2.2 milestone Jul 9, 2022
@tydeu tydeu closed this as completed in 080cda1 Jul 9, 2022
Kha pushed a commit to Kha/lean4 that referenced this issue Jul 17, 2023
@tydeu
feat: add shorthands for lake script run/list
958e3fc 
closes leanprover/lake#88
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees
No one assigned
Labels
enhancement New feature or request
Projects
None yet
Milestone
v3.2.2
Development

No branches or pull requests
2 participants
@arthurpaulino @tydeu