Re: [isabelle] automatically grade Isabelle homework?

Hi Joachim,

> besides adding security (which is better handled by containerization),

... a dubious amount at best. Using "code_printing" and "export_code"
you can already write arbitrary things to the file system, e.g.
".bashrc" or the checker theory (if those are writeable). Also let me
reiterate that the "secure" mode is gone after Isabelle2016.

> the safe mode also prevents the student from adding ML code that allows
> them to implement a bad oracle, i.e. their own "sorry", right? Will
> there be another way of avoiding that, once the safe mode is gone?

There are more ways to cheat than that, e.g. with "axiomatization" or
introducing custom or changing existing input/output syntax. However, ML
oracles can be easily detected using "Thm.peek_status" (the "oracle"
field is set to "true").

Given that the whole system is so complex there is no bullet-proof way
you can reasonably assign grades without reserving the right to deduct
points if cheating is detected by a human. (Human review of Isabelle
sources is a necessity.)


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.