Set up proper testing infrastructure

[javra]

Maybe see how mathlib4 and std4 run their tests.

[RaitoBezarius]

@javra So what I propose to this is:

(a) We can do the nightly testing branch where we bump all our dependencies, e.g. Lean 4 and Mathlib4 and run the tests over there and we can be pinged when the pipeline fails. (what Std4 does.)
(b) We can add something like Bors (Bors is deprecated though in favor of GitHub Merge Queues but they are not super nice), we can use https://mergify.com/alternative/github-merge-queue instead.
(c) We can adopt the classical labelling mechanism that those projects uses (awaiting for review, awaiting for author, merge conflict, etc.)

The rest of the files here:
https://github.com/leanprover-community/mathlib4/tree/master/.github/workflows

seems to be quite specific to the scale of Mathlib4, I'd say?

[RaitoBezarius]

Maybe, we can keep staying on a specific Lean 4 version though.

[javra]

I'm not against bumping everything manually and just giving all of us the power to merge instantly.

I think the most pressing thing is that we still test everything by just building the stuff, including commands that produce output, in Aegis.Tests and in mathlib they seem to have a solution where we have Foo.lean.expected.out files that are matched against the actual output.