search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
583 stars 236 forks source link

Streamlining the `make test`/CI infrastructure? #2248

Open jamesmckinna opened 10 months ago

jamesmckinna commented 10 months ago

Now that we use a merge queueing discipline for PRs, I'm conscious of inefficiencies in the 'mid-/post-review, but pre-merge' phase of commits to PRs, in that the CI seems to do a 'full' cycle not just of typechecking (incl. deprecated modules) and golden testing, but also of all the documentation/HTML index generation, which seems as though it would be more efficient to postpone (UPDATED: and even the golden testing phase?) until after adding to the merge queue?

There's a risk of errors only being exposed later in the cycle, but the gain would be faster turnaround in testing pre-merge.

JacquesCarette commented 10 months ago

Agreed.

MatthewDaggitt commented 7 months ago

Yes, if anyone is willing to take this on to optimise the CI in this way it would be much appreciated!

jamesmckinna commented 7 months ago

Currently, I don't have a good mental/actual model of the CI-infrastructure to do this myself. Sorry to be only the generator of 'user' gripes, rather than 'admin' solutions... !