Automatic marking with lean

Stream: general

[Thorsten Altenkirch]

I am using lean to teach our 2nd year module on logic. The student numbers are up and I am looking for a more efficient way to assess the coursework (it doesn't count for much but they need to do it). How can I set up lean so that the student can run a script which produces an output saying with theorems they have proved (without using sorry). Ideally I would also rule out the use of advanced tactics.

[Thorsten Altenkirch]

Sorry just saw that there is "Lean for Teaching".

[Alex J. Best]

I think some of the setups in lean for teaching are more robust, but if you just want something quick and easy and trust that students aren't trying to break the system you can use something like

import tactic
open environment tactic

run_cmd do
  e ← get_env,
  proved_thms : list name ← e.mfold [] (λ d l, do
    if (e.decl_olean d.to_name = none) ∧-- list decls in the current file only
        ¬ (`quot).is_prefix_of d.to_name ∧-- some axioms that are always there
        ¬ d.is_auto_or_internal e ∧ -- ignore junk
        ¬ d.value.contains_sorry then -- check for literal sorry or unfinished proof
      return (d.to_name :: l)
    else return l),
  trace proved_thms

there are countless ways to cheat such a simple system but its simplicity can also be useful, for instance students can use a sorried statement to prove an unsorried one and it will count. Completely formally this isn't a proof, but of course this might be a situation where we would still award the point (assuming the exercises depend on each other)