Merge PackageDistro, PackageDistroTools and gap-infra/integration repositories into one

[fingolfin]

I think this the most efficient all in all:

• the integration tests need the package distro anyway, and ideally the latest version
• we'd ideally like to run them our pull requests adding/modifying/removing packages, that is by far easiest if this is one repo
• all Github Workflows for the PackageDistro repo clone the PackageDistroTools into _tools, so we might as well have them as one?

Any thoughts, concerns, (dis)agreement, ... with this, @ChrisJefferson @james-d-mitchell @ThomasBreuer @wilfwilson ?

UPDATE: PR #130 merged PackageDistroTools into this repo.

[wilfwilson]

I never thought about this is too much depth, but my gut feeling before the GAP Days was always that the package integration tests belong with the package distribution.

I'd be happy for it to happen - although I realise that it'd take some effort! I note in particular that gap-infra/integration is (basically) just set up to whatever exists in the Docker containers, so some significant work is required; see gap-infra/integration#15.

[FriedrichRober]

@fingolfin, maybe Lucas and I can try to merge all three repos into this one? Certainly some work needs to be done, but this would be a good opportunity for us to understand how everything is roughly working and would make further work easier and more consistent.

In the process, we would also move all packages into a sub-directory, as suggested in #24 .

My only concern is, that a pull-request to this repo would not automatically mean that a package updated, so we would need to be a bit more careful with pull-request triggers in our actions.

[FriedrichRober]

Or we could add a branch _tools and use worktrees as I did for uploading reports to the data branch in gap-infra/integration#17

But this could be a bit fiddly.

[fingolfin]

See also issue #79: We already have to deal with commits that don't modify packages because we make some which just edit .github.

I've handled this (I hope) for PRs in PR #80: we can determine which files a PR adds/modifies/removes. It is less clear how to do this for "push" events to the main repo, as I am not aware of a way to determine what the previous revision was...

Hmm, but now that I write this, I think that perhaps we can just use the latest tag for that (at least for pushes to main).

[FriedrichRober]

@fingolfin, I tried to cherry-pick the PackageDistroTools into PackageDistro, but the merge-commits in PackageDistroTools cause me trouble. Do you know of a different approach to "merge" repos while preserving somewhat the history?

[fingolfin]

We've discussed this on gather and I think @FriedrichRober now used https://github.com/newren/git-filter-repo

[fingolfin]

UPDATE: PR #130 merged PackageDistroTools into this repo.

[fingolfin]

We may or may it merge the integration repo with this one, bit I see no value in leaving this issue open.