feat: lake: postUpdate? + test
#2603
Conversation
github-actions
bot
added
the
toolchain-available
leanprover-community-mathlib4-bot
added
the
builds-mathlib
|
src/lake/README.md
Outdated
| @@ -164,6 +164,7 @@ Lake provides a large assortment of configuration options for packages. | |||
|
|
|||
| ### Build & Run | |||
|
|
|||
| * `postUpdate?`: A post-`lake update` hook. The monadic action is run after a successful `lake update` execution on this package or one of its downstream dependents. Defaults to `none`. | |||
There was a problem hiding this comment.
Could we have an example? Looking at this diff, the only clue as to how to actually define such a hook is:
- reading the type
Option (LakeT LogIO PUnit) - looking at
src/lake/tests/postUpdate/dep/lakefile.lean.
If this is meant to help Mathlib run lake exe cache get after an update, then there needs to be an example in a documentation file that shows how to run an exe target as an update hook.
There was a problem hiding this comment.
@semorrison While I agree in spirit, I am not quite sure where to put such an example. Putting it here in the README would be awkward as none of the other configuration options have examples. Thus, giving it one would would draw the reader's attention, focusing them on an option that is likely not useful for most users. Would putting the example in the docstring be sufficient?
There was a problem hiding this comment.
Maybe start a new file? I don't really mind where it goes. If one option is better documented than others that's a good thing, and the "fix" is to document the others as well...
There was a problem hiding this comment.
I'm just hoping that we can say "Patrick, do you want to see if you can make lake exe cache get run automatically as part of lake update", and he replies with "Wow, that was easy" rather than "Option (LakeT LogIO PUnit)???".
There was a problem hiding this comment.
@semorrison Does the new docstring look good?
There was a problem hiding this comment.
The docstring is great, and I've verified that it works.
My only concern is about the code block in the comment eventually rotting.
- Maybe the API is uses is sufficiently stable to just not worry?
- Alternatively we could have a test that is effectively isomorphic (in terms of API calls) to the example in the doc-string, and a comment saying "If you need to fix this test, make sure you also update the doc-string on
postUpdate?".
I'm happy either way.
There was a problem hiding this comment.
@semorrison I went with option 2. If everything looks good, this feature should be ready to merge. 😄
tydeu
force-pushed
the
lake-post-update
branch
from
be65f16 to
e2d25ac
Compare
tydeu
force-pushed
the
lake-post-update
branch
2 times, most recently
from
a72b160 to
a908d58
Compare
tydeu
force-pushed
the
lake-post-update
branch
from
a908d58 to
362f269
Compare
Closes leanprover/lake#185.
This feature is implemented in a very straightforward mannaer. It is simply a monadic package configuration option.
lake updateruns all the workspace's packages'postUpdate?actions after resolving dependencies and finalizing the workspace but before writing the manifest to its file.