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 ?

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

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

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

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: May 18 2024 at 08:40 UTC