The Metamath set.mm repository has now switched from Travis CI to GitHub Actions for the CI pipeline.
Early experience by @avekens is positive; it’s MUCH faster & has easier navigation <https://github.com/metamath/set.mm/pull/1886>. One quirk: There are many jobs, and normally half of them skipped. We want to ensure that we run a check on every push inside the repo *and* pull request to the repo,. The only way I found to do that was to create jobs for both cases and skip execution when it’s a duplicate. This causes a few seconds’ delay (as it works out what jobs to run) & we see lots of skipped jobs, but that’s a price worth paying... we run the CI pipeline whenever it’s needed *without* doing a lot of duplicate work. --- David A. Wheeler -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/41D97171-3D8D-40B7-88D8-3B52D44E61BA%40dwheeler.com.
