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

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:

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.

Last updated: May 18 2024 at 08:40 UTC