GitHub mirror sync

(1) By Ryan Finnie (ryan) on 2020-07-20 21:23:37 [link]

After confirming [the CI builds are working well](https://github.com/tangentsoft/pidp8i/actions/runs/175286258) on both Ubuntu and MacOS runners (and producing tarball artifacts), I've merged the `github-ci` branch.

How often is the sync from Fossil to GitHub running?  It looks like the last one was a week between syncs, but before that it seemed to be daily, I think.  How "heavy" is the sync; i.e. could it be run hourly?  Every 5 minutes?  TBC we're still talking about an optional convenience which is not to be relied upon, but it would be useful for people to be able to see the CI results of a commit relatively soon after the commit is made.  (BTW, the GitHub workflow is configured to work on all branches, so it doesn't have to be a `trunk` commit.)

(2) By Warren Young (tangent) on 2020-07-20 21:47:52 in reply to 1

> How often is the sync from Fossil to GitHub running?

It used to be every day, and is now every hour.

The actual issue was a bug in the script that meant it only pushed the current repo state when I was testing from the machine that does the mirror update. Changes made on other machines weren't being pushed until I manually pulled them to the update machine first, so they could then be pushed.

Now the mirror update machine does a pull before push.

> Every 5 minutes? 

I get the value of a small feedback loop, but the repos I have mirrored to GitHub just don't change that often. It's hard to sell ~10000 null updates per week just so you can get an update 5 minutes after the first commit.

If it becomes a serious issue, there are methods to avoid a bunch of useless round-trips with GitHub while still pushing quickly.

(3) By Ryan Finnie (ryan) on 2020-07-20 22:04:01 in reply to 2 [link]

Excellent, thank you!

> I get the value of a small feedback loop, but the repos I have mirrored to GitHub just don't change that often. It's hard to sell ~10000 null updates per week just so you can get an update 5 minutes after the first commit.

Agreed.  If the sync script were complex enough that it was maintaining a state knowing what was last pushed to GitHub, every few minutes would be trivial, especially if there's nothing remote to do.  But for a basic blind pull/convert/push operation, I think hourly is an acceptable sweet spot.