> 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.
As I said in the issue, I think this is the right approach. Besides the boilerplate associated with setting up CI, I don't think there is any complexity to the current travis script - it's just a list of commands that could just as well be in a bash script and called from anywhere. The details of triggers on GA are a bit different but it's quite flexible and I don't think supporting a separate nightly build is a huge extension so much as a rearrangement of lines. That said, I'm personally pretty procrastinatory about this stuff - I've been putting off setting up MM0 CI via github actions for months, which I'm sure would be valuable experience here - so it mostly just comes down to looking up the API and making the switch. Mario On Wed, Nov 18, 2020 at 9:33 PM David A. Wheeler <[email protected]> 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/93F3FE08-A42B-48F3-BD9A-1FD489FE3C87%40dwheeler.com > . > -- 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/CAFXXJStPVW1TVPBbj5ZmZhAmzAsPOTzc66rTfN0NZPUd%2ByezoQ%40mail.gmail.com.
