5 ms·

> The 25 minute value is only the time to verify a single Coq proof. Logically it is a singe proof, but technically it consists of quite a few theorems and lem

• digama0 7y ago
  It goes without saying that metamath is not designed to be read from the source directly. To be perfectly fair, Coq isn't either; you can kind of get the gist but to really understand what's going on you have to start up Coq and look at proof states. Metamath as it's meant to be seen looks like this: http://metamath.tirix.org/f1o2ndf1.html http://metamath.tirix.org/f1o2ndf1.html . I agree that calling it "one proof" is a mischaracterization, but comparing all of Raft to all of set.mm is probably about right. I would guess set.mm is 10-100 times larger than Raft in terms of number and complexity of actual proof content, but it checks in a fraction of the time, in part because of that "core dump". You might think it ugly, but have you ever looked at a .vo file? The difference is metamath checks its 'cache' in to version control.
  • h91wka 7y ago
    > The difference is metamath checks its 'cache' in to version control. As I said in the initial post, there is an entire world of difference between checking the proof term and, well, proving. Coq can dump proof terms that can also be verified relatively quickly, but typically people prefer to run proof scripts in CI. And proof scripts actually search for the proof, rather than simply describe it. So, travis run time is not a terribly precise metric. As for comparing the number of lemmas... In Coq one has "magical" tactics such as `omega' or `lattice'. Metamath doesn't have tactics (?), so I presume that's the reason they need so many lemmas in standard library; just like you need 100x time more code in asm than in Haskell.
    • digama0 7y ago
      Metamath has tactics, but they aren't part of metamath per se; they are part of the tools that you use to write proofs. You don't make the rest of the world run the same proof search you did hundreds of times, finding the same proof every time, when you could just write down the proof. I'm aware this is an entirely unfair comparison. Coq and Metamath aren't doing anywhere near the same amount of stuff, so of course Metamath will be faster. But the question is: are you doing what is necessary? Is running omega all the time a requirement for large scale proof checking, or is it just the way Coq does things? I think you will find that it's not necessary in the abstract, but it's also pretty hard to write Coq any other way. (To be absolutely clear, I don't mean don't use omega, I mean use omega once and generate a proof, and don't make the rest of the world have to re-run your proof script.) The sizes of things are actually hard to gauge in Metamath if you want to compare LOC to amount of human work, because what you see in a Metamath file are actually the output of some honest to goodness "tactic" or high level user interface. No one is writing asm here. If you are not writing lemmas, and are relying on Coq tactics to rediscover the proof all the time, well, that's just demonstrably slow and redundant. In Metamath we use a combination of tactics to find proofs and optimizers to extract common lemmas and use the library of existing lemmas effectively; the Coq model leaves no space for the optimizer, so you get something... suboptimal.