All sounds good, thanks for looking into this.
I'd say that running everything on every pull request would be my
preference, and I don't think it takes that long to run (at least, it
hasn't on travis). Nightly is an option if we have to, but if the
nightly run fails there is a debugging step of figuring out which of the
pull requests merged that day caused the problem.
On 11/18/20 6:33 PM, David A. Wheeler wrote:
All:
I propose that we move from using Travis CI to something else, probably GitHub
Actions, for the set.mm repo. This is proposed here:
https://github.com/metamath/set.mm/issues/1867
I intend to work to implement this, though help is always welcome. Details
below.
--- David A. Wheeler
=== DETAILS ===
One great thing about the set.mm repository is that every proposed change is
examined by multiple checking tools (including a number of verifiers). This helps
provide extraordinarily high confidence that the proofs follow from the given
axioms & definitions. While it focuses on the set.mm database, there are also
checks on set.mm (based on intuitionistic logic). This checking of each potential
change is a normal process in software development, and is often called a
continuous integration (CI) pipeline. The CI pipeline for the set.mm repository is
implemented using Travis.
Unfortunately Travis has become increasingly unreliable, showing as increasing
delays or occasional unexpected failures. There are also reasons to think we
may not be able to use it in the future. Travis has been having a number of
problems as a company; those who are curious about more can look at these:
https://www.jeffgeerling.com/blog/2020/travis-cis-new-pricing-plan-threw-wrench-my-open-source-works
https://blog.travis-ci.com/2020-11-02-travis-ci-new-billing
https://news.ycombinator.com/item?id=25003387
I propose switching to something else. The “obvious” answer is GitHub actions.
It’s free for OSS (and we are), and we’re already on GitHub. This basically
requires creating a new .yml file to implement it. GitHub actions trivially
supports parallel jobs.
I intend to start implementing this. Someone else had done a first step at
that, so I’ll certainly look at that.
Mario would like to see fewer verifiers run on *each* commit, and instead run
the “rest” of the verifiers separately (e.g., nightly). I’m skeptical that will
save anything we care about, and doing that will complicate things. More
importantly, trying to make that change *and* simultaneously moving our jobs
from Travis to GitHub Actions is more complex.
So I intend to move the Travis jobs to GitHub Actions *first*, while doing my best
to isolate the jobs. We can then *separately* consider if we should split jobs into
“nightly” and “per-commit” jobs, and how to split them, once we have confidence
that the jobs have been correctly moved. It’ll be much easier to discuss trade-offs
& implementation difficulty once we have our CI pipeline moved to a more
reliable service.
--
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/2e344656-52bb-5d83-1634-d92c89bf90a7%40panix.com.
