Re: [isabelle] automatically grade Isabelle homework?
> 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
Checker.thy â contains the exact same lemma statements, but using a
proof "by rule".
theory Interface imports Main begin
definition prime ...
theory Student imports Interface begin
lemma no_biggest_prime: obtains p where "prime p" "p > n"
theory Checker imports Interface Student begin
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"
* 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:
> 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/...
This archive was generated by a fusion of
Pipermail (Mailman edition) and