search

klapaucius / vector-hashtables

Other
33 stars 5 forks source link

Adding Agda to CI? #30

Open ulysses4ever opened 6 months ago

ulysses4ever commented 6 months ago

Agda is a big (the biggest?) consumer of our package. It'd be nice to make sure that many little changes we've been applying recently don't break anything particularly badly on their side, and at least give them a heads-up if it breaks.

OTOH Agda is a big project to add to the regular CI carelessly. In theory, we could run it by corn or on merge instead of on pull.

@andreasabel -- any suggestions/advice on this?

andreasabel commented 6 months ago

@ulysses4ever wrote:

run it by corn

Sorry, my vocabulary fails me here. What does this mean?

andreasabel commented 6 months ago

Ah, this is probably a typo, "cron". Ok. Yeah, maybe a cron job would do it. What do you want to test? Just functionality or also performance?

ulysses4ever commented 6 months ago

Oh my, sorry: I meant cron, which means on a schedule. GitHub actions can do that afair.

ulysses4ever commented 6 months ago

We thought functionality for starters.

andreasabel commented 6 months ago

Maybe you could have agda and agda-stdlib as submodules pinned to released versions (v2.6.4.3 and v2.0 resp.) and build agda with your master and run it against its standard library.

Running the whole testsuite of Agda is maybe not what you want. This is how we do it: https://github.com/agda/agda/blob/403ee4263e0f14222956e398d2610ae1a4f05467/src/github/workflows/test.yml