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.
