patching a dependency in lake

Stream: general

[Robin Carlier]

Say I have a .patch for a repo (e.g Mathlib), and a project downstream of that repo. Is there a way to have lake apply that patch locally to the upstream repo? Or is there no better way than maintaining a mirror of the repo?

[Ruben Van de Velde]

No, maintaining the fork is the way to go

[Mac Malone]

One possiblity is to write a post_update hook to apply the patch. See Mathlib's hook for an example of what a hook in general looks like. However, a fork is the more straightforward way to do this.

[Kim Morrison]

Make life sane by either PR'ing your patch, or deciding to do without it. :-)

[Robin Carlier]

Kim Morrison said:

Make life sane by either PR'ing your patch, or deciding to do without it. :-)

It's actually already done, but through different (not yet merged) independent PRs in mathlib that I'd like to combine.
And I feel like even as a draft, making a branch combining them for my other projects is just plain abuse of my write access to the repo.

[Yury G. Kudryashov]

IMHO, it's OK if you don't forget to delete the branch once you don't need it anymore.