Re: [isabelle] automatically grade Isabelle homework?



Dear Johannes,

> 1. what is the best way to pattern-match
> student's Isabelle code against problem statement?
> For Haskell, I actually compare abstract syntax trees.

is there any reason you require students to exactly fill out holes? For
our Haskell course we reckoned a "matching interface" is good enough.

In Isabelle you could get something similar by using three theories:

Interface.thy â definitions would go in there
Student.thy â lemma statements + sorry would go there, student has to
fill them
Checker.thy â contains the exact same lemma statements, but using a
proof "by rule".

Example:

Interface.thy

  theory Interface imports Main begin

  definition prime ...

Student.thy

  theory Student imports Interface begin

  lemma no_biggest_prime: obtains p where "prime p" "p > n"
  sorry

Checker.thy

  theory Checker imports Interface Student begin

  lemma check_no_biggest_prime:
    obtains p where "Interface.prime p" "p > n"
  by (rule Student.no_biggest_prime)

Depending on where exactly a failure occurs (you can put those into
multiple sessions) you know where the student did something wrong.

> 2. how safe is it to run Isabelle? - For Haskell,
> anything dangerous would be in IO, which is prohibited
> by putting type annotations in the problem statement
> (which the student cannot change).
> And "unsafePerformIO" is prohibited because it would need
> some "import" statement - which again would not survive
> the pattern matching. So, the worst that can happen
> is that student's code runs forever,
> and for that I just limit execution time (to a few seconds).
> Is there any way to sneak an IO action into a proof?

Isabelle allows arbitrary code execution. There is currently a "safe"
flag but:
* with that many legitimate things don't work
* it will be gone in the next release.

I strongly recommend containerizing Isabelle for running untrusted code.
(We use unprivileged containers without network access in a VM in our
AFP submission checker.)

On the plus side, setting timeouts is possible and robust.

> 3.1 How would I run Isabelle? Of course I don't want the GUI.

You have to prepare a ROOT file and put all the files into appropriate
folders. Then you can run

$ bin/isabelle build ...

See also Â2 in the Isabelle system manual:
<https://isabelle.in.tum.de/dist/Isabelle2016/doc/system.pdf>

> 3.2 Can I avoid putting student's submission in a file,
> and pipe it instead?

You could, but that would involve you writing some nontrivial amount of
custom Scala code to drive the build process. I wouldn't recommend it.

> 3.3 How would I detect that Isabelle actually verified the proof?
> Ideally, just by checking the return code?

Yes, you get that for free from "isabelle build". Exit code 0 means
session built successfully, other exit codes mean timeout/failure/...

Cheers
Lars




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