Kevin Lacker (Nov 09 2020 at 19:09): Kevin Lacker (Nov 09 2020 at 19:09):Hey, I was looking around for samples of Isabelle code and I ran across the "archive of formal proofs" at https://www.isa-afp.org/index.html . But, it seems like it is a bunch of PDFs. Do people use that in some way? Is there something like, a github repository with this code?
Kevin Lacker (Nov 09 2020 at 19:35):well, i managed to prove this great work of mathematics:
lemma foo: "2 + 2 = 4"
by auto
If you go to the 'About' link on the menu on the left, you can find your way to a repository. You can also download all the entries from the 'Download' link on the left. Or you can browse the theory files in each entry from the 'Browse theories' link in the page for each entry.
Kevin Lacker (Nov 09 2020 at 19:44):ok cool. do you know if there's any particular reason this doesn't use github?
Mathias Fleury (Nov 09 2020 at 19:51):On the one hand: why would they use github?
On the other hand: historically, isabelle uses mercurial and github only supports git. And some people complain loudly about github.
Kevin Lacker (Nov 09 2020 at 19:53):i was just curious because i looked on github first and didn't see anything. but it makes sense if isabelle folks are attached to mercurial
Last updated: Dec 21 2024 at 16:20 UTC