Simon Wimmer (Jul 01 2020 at 07:44): Simon Wimmer (Jul 01 2020 at 07:44):One specific item we would like to discuss are libraries:
it is clear that Isabelle/HOL has an extensive standard library, while Coq's is small, and Lean is somewhat in between.
For this reason, we opted for allowing people to pull in other libraries with the rationale that a) things can always be copied in anyway and b) that knowing your libraries is part of the game.
However, this is also tricky because it is not really possible 'to just pull in' any library in Coq afaik.
Manuel Eberl (Jul 01 2020 at 08:26):Yeah, libraries are a tough problem. I don't think there's a good solution there. It's always a gamble.
I would however say that a) is only half true because copying in stuff is not so easy: You can only submit one thy file, so you have to copy everything and its dependencies into your theory file and deal with whatever fallout that causes and stay below the time limit. Plus, you might have to write glue code between the definitions from the problem file and that library, so that in the end, it's easier to just do everything from scratch.
b) on the other hand is a good argument, but it may lead to perceived unfairness because then some problems might become much easier in a system that has a library for the task than in another that does not. Of course, that is still the case even if you only allow the most basic standard library, but it becomes more of an issue the bigger the library is.
Personally, I feel that everything in the Isabelle distribution should be okay to use, but the AFP probably shouldn't. But with e.g. HOL-Analysis, importing it would probably immediately break the time limit because it takes about 3 minutes to build even on a really beefy machine, so for problems for which that could be useful, you should ideally load that as an image in your checker. In any case, the theories in HOL-Library can be imported individually and would sometimes come in really useful.
I don't know what exactly the situation is like in the Lean and Coq world, so I can't comment on that.
maximilian p.l. haslbeck (Jul 01 2020 at 08:28):For Isabelle we already prebuild sessions, although we do not make that transparent to the contestants.
Manuel Eberl (Jul 01 2020 at 08:30):By the way, it would be nice to have some more clear information about what you are allowed to include. I was under the impression that I can't include anything that isn't from the HOL session.
Simon Wimmer (Jul 01 2020 at 08:36):Yeah I agree that it should also be stated more precisely. We simply forgot to mention it this time :grinning:
Athough, we should probably never provide a pre-built HOL-Analysis image.
Kevin Kappelmann (Jul 01 2020 at 08:37):All of Lean and its external mathematical library are also pre-build.
Last updated: Apr 24 2024 at 12:33 UTC