Run CI on a fork's branch?

Stream: lean4

[Thomas Murrills]

Sometimes I'd like to run CI on a branch on my own fork of lean4 without polluting the main repo with draft PRs (which has been my M.O. thus far! :) ).

I know I can do this by making a tag and a release, but this seems like a lot of menus to click through; if this is the preferred (non-PR) way, that's fine! It just feels like I'm missing something—I'd imagine there'd be something more direct to click (or, at worst, some CLI command to run) that just means "run the workflow on this branch" without making a tag each time.

(I tried commands like gh workflow run 'PR release' --ref <branch>, but this gives me errors about lacking a "workflow dispatch event".)

[Kim Morrison]

Somehow your question is phrased in a way that is very hard to answer.

No? Yes? (You must make a PR, or tag, or work out how to modify CI yourself. :-)

[Thomas Murrills]

I believe the reason it's hard to answer is that I did not, in fact, include a question after all. Oops. :upside_down:

But I think that parenthetical answers the question I meant to ask, which is "do you need to make a tag or PR to run CI (given the way it works currently)". :)

A follow up question is: if you run CI by making a tag, do you need to make a new tag each time you want to run CI on a branch? (I'm wholly unfamiliar with tags.)

[Sebastian Ullrich]

You can force-update tags. You don't need to create a release for them. You can also make PRs to your own fork.

[Thomas Murrills]

Ah, okay! Googling got me to git tag -f <tag> <branch>, which seems promising. (Knowing that tags are meaningful independently from associated releases is useful too, since this isn't obvious when poking around the GitHub website!)

[Jon Eugster]

In my own workflows I usually have the following:

on:
  workflow_dispatch:

which allows you to click a button to run the workflow manually and select the branch to run it on (or trigger it via the command you mentioned, I assume)

I would guess you could just add this to the desired workflow on your fork (I think the modified workflow needs to be on main/master?)

[Jon Eugster]

(but PRs against the fork's main is what I do even more often)

[Thomas Murrills]

Oh, clicking a button like that sounds like what I was looking for! (Though admittedly I too might wind up just using PRs against my main, now that I know that works.)

Though, if the workflow modification is on your main, does that mean that syncing with leanprover/lean4 (and/or making branches which don't include that change) is awkward? I could imagine accidentally making a new branch based on my fork's main, making a real PR, then realizing I have to remove on:\n workflow_dispatch.

[Jon Eugster]

updating is probably just a simple git rebase upstream/main once you added leanprover/lean4 as upstream, havent tested if the website "Sync" button does that, too, but I would guess so.

but keeping such a tmp commit out of your branches might need a bit manual care, indeed