Stream: jsCoq

Topic: jsCoq / Learning tools interoperability


view this post on Zulip Julien Narboux (Apr 25 2022 at 13:20):

For teaching maths using a proof assistant for a large group of students, I am currently using Edukera, I would be interested into moving to Coq, for this purpose it would be interesting for me to have support for LTI standard ( https://www.imsglobal.org/activity/learning-tools-interoperability) to be able to add exercises inside Moodle. Support for LTI allows to identify students and teachers, and to obtain the grades automatically inside Moodle. Have you ever considered LTI integration ?

view this post on Zulip Shachar Itzhaky (Apr 25 2022 at 16:18):

Wow I had no idea this was standardized to such a level. Are you familiar with the SF grading scripts? They can produce a point grade for student's answers based on how many lemmas are proved. We were thinking of integrating their autograder with the SF site (coq.now.sh/ext/sf).

view this post on Zulip Bas Spitters (Apr 26 2022 at 08:04):

It would be nice to also integrate with github classroom, and I guess gitlab has something similar: https://about.gitlab.com/solutions/education/

view this post on Zulip Emilio Jesús Gallego Arias (Apr 26 2022 at 16:52):

That's very nice, please open an issue for both in the jsCoq repos !

view this post on Zulip Bas Spitters (Apr 27 2022 at 08:12):

Note that github seems to only support LTI 1.0 and 1.1. Gitlab does not seem to support LTI.
https://docs.github.com/en/education/manage-coursework-with-github-classroom/teach-with-github-classroom/connect-a-learning-management-system-to-github-classroom


Last updated: Jan 31 2023 at 09:01 UTC