Hi everyone,
(reposting here the announcement on coq-club)
We are happy to announce a new proving contest at Proving for Fun, an online platform where you can tackle proving challenges in your favorite proof assistant:
https://competition.isabelle.systems/competitions/contest/11/
While the platform was initially targeted at the Isabelle proof assistant, this month’s contest features freshly implemented support for Coq! This means you can now submit your solutions in both Isabelle and Coq. The contest is open starting now until 9 August 2019.
This also serves as a warmup for the “Proof Ground” workshop [1], which will take place in September alongside the ITP conference in Portland. The goal of the workshop is to bring together researchers from the ITP community, to discuss and compete in a “proving contest”, and it will use the Proving for Fun platform. If you happen to have ideas for interesting tasks, please consider submitting them following our “Call for Problems”.
We believe our problems should be a stimulating fun summer activity! We encourage you to participate and give us feedback on the prototype system.
Happy proving,
Max Haslbeck, Simon Wimmer, and Armaël Guéneau
8 Likes
On a more technical note, I want to thank @ejgallego and @palmskog for their great help with using serapi, that I use crucially in the Coq backend of the grading system.
This looks interesting (and I was happy to help out with SerAPI).
However, is there some detailed breakdown of what the backend validation environment looks like? Is it Coq 8.9.1 and only stdlib?
For example, SSReflect/MathComp users (including me) would likely want to access to at least coq-mathcomp-ssreflect.1.9.0.
At the moment, the backend environment is coq 8.10 and only the stdlib (the rational behind chosing 8.10 was to limit the number of known soundness bugs).
Nevertheless, I think it should be easy for me to opam install packages in the switch of the backend, as long as they work with 8.10. Then, you should be able to simply Require Import them in your submissions.
Note that (unless I overlooked something) I checked that the tasks can be completed reasonably using only the stdlib and the (small) background definitions provided in Defs.v. Generally speaking, we tried to make the tasks reasonably self contained, so that they do not get trivialized by an ITP that happens to have the right background theory in its standard library.
I’ll look into adding coq-mathcomp-ssreflect :-).
Update: coq-mathcomp-ssreflect is now available!
1 Like
Great @Armael, it looks so fun! As discussed on Gitter you may want to disable the VM, and check that some options such as type in type are not available as Set commands. Also, I recommend you apply the patch for https://github.com/coq/coq/issues/9294