FYI, we now have a number of verifiers that run in parallel when changes are made to the "set.mm" repo (which includes set.mm and iset.mm).
You can see an example here: https://travis-ci.org/metamath/set.mm/builds/600478951 They run as a bunch of parallel jobs: * smetamath-rs (Rust, Stefan O'Rear) verification * mmj2 (Java, Mel L. O'Cat and Mario Carneiro) verification * Metamath.exe (ISO C, Norman Megill) verification * checkmm (C++, Eric Schmidt) verification * mmverify.py (Python3, Raph Levien) iset.mm verification * mmverify.py (Python3, Raph Levien) set.mm verification (skipping mathboxes) * Date validation (of set.mm) Since the verifiers run in parallel, adding new verifiers does not necessarily make verification any slower. The program mmverify.py is in Python, which is very slow. To prevent its time from overwhelming the rest, I'm rigged things so that checking iset.mm and checking set.mm are separate parallel jobs, and the mmverify.py checking of set.mm skips the mathboxes (it *could* check mathboxes, but that would take longer). Notice that the validators are in different languages & are by different people. We now have 5 validators (though mmverify.py doesn't normally check the set.mm mathboxes due to speed issues). I claim that having multiple validators, in different languages by different people, increases the likelihood of detecting a mistake in a proof. I certainly don't know of any other suite of math proofs that passes so many independently-implemented validators. --- 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/E1iMNL3-0002uV-LV%40rmmprod07.runbox.
