Skip to content

Setup for autograding of Lean homework using GitHub Classroom

License

Notifications You must be signed in to change notification settings

mattrobball/lean-autograding

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

59 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Automatic grading of mathematics assignments with Lean and GitHub Classroom

We provide a basic setup that integrates the Lean Theorem Prover with GitHub Classroom.

Why GitHub Classroom?

The advantages of GitHub Classroom for an instructor include:

Why Lean?

The Lean Interactive Theorem Prover is powerful language for expressing sophisticated mathematicial structures and for verifying correctness of arguments.

With a Lean verified proof, you can be sure of correctness.

Autograder configuration

The autograder action is configured using .github/classroom/autograding.json. This controls the tests.

The fields are

  • name: a name you give to each test to run, e.g. Exercise 5
  • setup : shell command to run for setup
  • run : the actual command for scoring the assignment. If it outputs to stderr it triggers a failure but this can be congifured using fields below
  • input : additional input to your run command
  • output : comparison output to that for run
  • comparison : how to compare, either exact, included, or regex
  • timeout : how long to wait in milliseconds until skipping the test
  • points : possible points for the test

Our setup

We use the setup command to runthe elan install script and then call leanpkg in directory root.

The file .test/test.lean imports src/assignment.lean and tests that an exercise of the form

lemma exercise : S

has produced a term of the correct type T with

theorem check : T :=
begin
  exact exercise, 
end

For the test we run lean .test/test.lean.

If assignment.lean has errors or warnings, the test fails as these propogate to test.lean.

If exercise has the wrong type, then the test fails.

So far this is fairly basic but suffices for assignments where you provide the lean template and students have to fill in the proofs sorry-free.

How to deploy

First, clone this repository to your account. Then edit assignment.lean and test.lean to fit your needs.

When creating your assignment, select your repository as the template repository.

About

Setup for autograding of Lean homework using GitHub Classroom

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages