Did anyone have success using github for education for teaching classes on Coq?

https://classroom.github.com/

https://education.github.com/

The autograder in SF should integrate quite well with the CI.

we have at least two efforts that builds fine-grained general autograding on top of Coq: https://www.codewars.com/kata/search/coq https://coq.discourse.group/t/proving-for-fun-summer-edition/351

however, integrating either of them with GitHub Actions would likely take quite some engineering work

for example, I don't even know what the status is on checking used axioms against a whitelist, I know there was a Coq issue along those lines...

SF provides an autograder. However, the most important check is that the whole file compiles.

github allows one to run an IDE via repl.it. It would be nice to have coq support for it, but I haven't look into how difficult that would be.

It does support ocaml.

in my experience, students do terrible things that still compile, no matter what tool/language

@Bas Spitters also, the autograder is not publicly available, right?

Autograder is e.g. BasicsTest.v in the tar file here:

https://softwarefoundations.cis.upenn.edu/lf-current/

presumably, this is not what Benjamin is referring to here: https://stackoverflow.com/a/45461908 -- or it is? I think `BasicsTest.v`

is autogenerated somehow.

Yes, that's the one we're using.

There is a more elaborate script, but I'm not sure we need it yet.

It would be nice to expand the autograder by using quickchick.

Github Classroom is very nice. It also provides collaborative online editing via repl.it

I've requested Coq to be added, in case people are interested.

https://repl.it/talk/ask/Adding-the-Coq-language/52498

Last updated: Dec 07 2023 at 06:38 UTC