Stream: Miscellaneous

Topic: Github for education

view this post on Zulip Bas Spitters (Sep 04 2020 at 12:31):

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.

view this post on Zulip Karl Palmskog (Sep 04 2020 at 12:35):

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

view this post on Zulip Karl Palmskog (Sep 04 2020 at 12:36):

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

view this post on Zulip Karl Palmskog (Sep 04 2020 at 12:37):

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...

view this post on Zulip Bas Spitters (Sep 04 2020 at 13:01):

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

view this post on Zulip Bas Spitters (Sep 04 2020 at 13:03):

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.

view this post on Zulip Karl Palmskog (Sep 04 2020 at 13:03):

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

view this post on Zulip Karl Palmskog (Sep 04 2020 at 13:06):

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

view this post on Zulip Bas Spitters (Sep 04 2020 at 13:26):

Autograder is e.g. BasicsTest.v in the tar file here:
https://softwarefoundations.cis.upenn.edu/lf-current/

view this post on Zulip Karl Palmskog (Sep 04 2020 at 13:27):

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.

view this post on Zulip Bas Spitters (Sep 04 2020 at 13:54):

Yes, that's the one we're using.
There is a more elaborate script, but I'm not sure we need it yet.

view this post on Zulip Bas Spitters (Sep 04 2020 at 13:56):

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

view this post on Zulip Bas Spitters (Sep 06 2020 at 15:04):

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: Jun 01 2023 at 12:01 UTC