linter for helping grading

Stream: Lean for teaching

[Alexandre Rademaker]

After watching the presentation https://youtu.be/5HDlgsjO8-w given by @Gabriel Ebner, I realized that I could use linter to give feedback for the students' code. I am currently using Lean in a discrete mathematics course hosted in GitHub, using the GitHub classroom to create assignments. https://leanprover-community.github.io/mathlib_docs/tactic/lint/basic.html#linter. Does anyone have experience with that? Some directions or examples that can give me some ideas on how to use it?

[Rob Lewis]

That's an interesting idea, I hadn't thought of using the linter like this!

[Rob Lewis]

A linter is very simple under the hood. It's basically just a function declaration -> tactic string.

[Rob Lewis]

So if you know enough metaprogramming to implement what you want to test for, hooking it into #lint is trivial.

[Rob Lewis]

But I think deciding what to test for his the hard part. It will depend a lot on what you're teaching your students to do.

[Rob Lewis]

Note that the linter framework doesn't look at source code, it works at the declaration level. So it won't help with formatting, syntax errors, things like that.

[Rob Lewis]

One cool teaching application could be to hook it up to @Simon Hudon 's new counterexample generation. Students could state lemmas they're trying to prove but not finish all of them. They run #lint at the bottom and it could report if it detects that any of the lemmas are unprovable.

[Rob Lewis]

Our paper on the linter is here and if you have ideas of what you'd like to test for I'm happy to give suggestions. There are some simple linters that you could use as examples if you want to implement your own.

[Patrick Massot]

Alexandre, do you ask students to define stuff and state lemmas? That sounds very ambitious, unless the core topic of the course is interactive theorem proving.

[Alexandre Rademaker]

Hi @Patrick Massot, well, that a good question. Discrete mathematics is a broad topic and we can focus on many different areas, right? I choose to follow the @Jeremy Avigad as much as I can. That means I use "logic and proof" from chapters 1-18. For the last part, I need to add something about graphs. For the natural numbers, I am planning to present them the natural numbers game from @Kevin Buzzard and play together during some lectures.

For the graph part, it is not clear yet if I can use Lean, I am still thinking about it, maybe I will present some code in Haskell. Last time I have some lectures about the PHP principle and combinatorics, but I was asked to present an introduction to graph theory this semester. For the first part on logics, besides the exercises from "logic and proof", I present students with some puzzles to be formalized and proved and also with a list of many LP and FOL tautologies to be proved. So they don't have to state very complex lemmas by themselves, but they learn to formalize basic stuff. They learn to make ND by hand first and to translate it to Lean. What happens that is many times their code is quite messy and I try to give as much feedback as I can to teach them that clean and simple presentation is an important part of the game.

[Patrick Massot]

The linter framework won't inspect proofs for you.

[Patrick Massot]

You wrote you want to follow Kevin and Mohammad's natural number game, but this is the extreme case of not allowing to write any statement.

[Patrick Massot]

I don't know whether Logic and proofs include exercises when you need to state or define something.

[Rob Lewis]

Patrick Massot said:

The linter framework won't inspect proofs for you.

Hmm? It can certainly inspect proof terms, and if they're written in the structured L&P style, it could be able to detect some worthwhile stylistic things.

[Patrick Massot]

But again I don't claim you shouldn't do it, only that it's very ambitious.

[Rob Lewis]

For example, I think you can write a linter that checks if a proof contains a have statement that isn't used.

[Patrick Massot]

Oh, proof terms... I always forget about those.

[Alexandre Rademaker]

Hi @Rob Lewis, where can I read more about the counterexample generation from @Simon Hudon ? Thank you for the links, I will try to learn more about it. that may be a stupid question but, once you have the lint tactics implemented, how do you use them to check the mathlib pull requests?

[Rob Lewis]

What they can't check are proof scripts, the input syntax. Even a tactic proof creates a proof term and depending on what you're looking for, you can certainly extract useful info from them.

[Patrick Massot]

Yes, of course checking for unused arguments is the canonical example.

[Alexandre Rademaker]

Patrick Massot said:

I don't know whether Logic and proofs include exercises when you need to state or define something.

Yes, sometimes I add bits of extra stuffs not in logic and proof. I do show them def and some type theory. Actually, I am learning that hidden type thoery makes things more difficult. The Hitchhiker’s Guide sequence for presenting Lean and logics in Lean now makes a little bit more sense to me.

[Alexandre Rademaker]

Patrick Massot said:

You wrote you want to follow Kevin and Mohammad's natural number game, but this is the extreme case of not allowing to write any statement.

The ideais is that once they know how to make term mode proofs, why not also introduce tactic mode and more applied logic to do mathematics.

[Alexandre Rademaker]

Rob Lewis said:

For example, I think you can write a linter that checks if a proof contains a have statement that isn't used.

That kind of check would be nice. I don't know why, but they loved have. They overuse it (for my personal perspective)

[Rob Lewis]

Alexandre Rademaker said:

Hi Rob Lewis, where can I read more about the counterexample generation from Simon Hudon ?

Simon is in the process of adding it now, there are some open PRs. The basics are there in the testing directory and tactic/slim_check. Maybe best to call @Simon Hudon directly for details though. In particular I don't think it's set up for pure prop logic yet, although I don't see why it couldn't be. It's very much actively in development.

example (p q : Prop) : p → q :=
begin slim_check end -- no testable issue

[Simon Hudon]

@Alexandre Rademaker It's still very new so there's still a lot I need to write. Fortunately, I'm not the first to implement such a tool and anything you learn about Haskell's QuickCheck will be informative about slim_check (the Lean port). And you can always ask if there's more to know.

I'm hoping the header comment in tactic/slim_check.lean will get you started

[Alexandre Rademaker]

Patrick Massot said:

Yes, of course checking for unused arguments is the canonical example.

Yes, in my last list of exercises, many students forgot extra hypothesis in lemmas, possible driven by the copy and past discipline...

[Simon Hudon]

@Rob Lewis the issue you're showing is that we can't print prop. That should change soon through a bit of hackering that I'm doing right now. In the mean time, you can go with bool

[Rob Lewis]

Alexandre Rademaker said:

that may be a stupid question but, once you have the lint tactics implemented, how do you use them to check the mathlib pull requests?

Not a stupid question, it's kind of complicated actually! The short story is, we build a file that imports all of mathlib (scripts/mk_all.sh) and run #lint_mathlib. Complications come because there are still lots of whitelisted exceptions from before the linters existed. We have a file of allowed exceptions that we add the @[nolint] attribute to before running the tests.

[Rob Lewis]

It's mostly done here

[Alexandre Rademaker]

Oh.. thank you. So in the end is the processing of this file that checks the mathlib library. Wow! I still have too much to understand...

[Rob Lewis]

Yep. But again, this file is a complicated way to write

import all

#lint_mathlib

because it has to import and update the whitelist of old declarations.

[Alexandre Rademaker]

@Simon Hudon , thank you for the pointers. I will take a look. Presenting logics from a proof theoretical perspective always make students question how to know if a formula is NOT provable. For answering that, I have to anticipate the LP and FOL semantics, present tools for truth table constructions, talk about ATPs, undecidability of FOL, etc. Having some way to present in Lean counterexamples would be definitely a useful tool.

[Kevin Buzzard]

@Simon Hudon when you print a prop will it just display as true or false?

[Simon Hudon]

Yes, that's the plan

[Rob Lewis]

Proof of concept, here's an "unused haves" linter. have is represented as a macro and there's no API for dealing with macros, so this took some reverse engineering and is probably overfit to the two examples I started with. But, it catches those and doesn't flag any other errors in mathlib up to that point, so...

import tactic

lemma foo (p : Prop) : p → p :=
assume hp : p,
have hp2 : p, from hp,
show p, from hp

lemma fun_problem (p : Prop) : ¬ (p ↔ ¬ p) :=
assume hpnp,
have hnp : ¬ p, from
  assume hp : p,
  have hnp : ¬ p, from hpnp.mp hp,
  show false, from hnp hp,
have hp : p, from
  have unnecessary : ¬ p, from hnp,
  show p, from hpnp.mpr hnp,
show false, from hnp hp


open tactic declaration expr

meta def expr.has_zero_var (e : expr) : bool :=
e.fold ff $ λ e' d res, res || match e' with | var k := k = d | _ := ff end

meta def find_unused_have_macro : expr → tactic (list name)
| (app a a_1) := (++) <$> find_unused_have_macro a <*> find_unused_have_macro a_1
| (lam var_name bi var_type body) :=  find_unused_have_macro body
| (pi var_name bi var_type body) := find_unused_have_macro body
| (elet var_name type assignment body) := find_unused_have_macro body
| (macro md [lam ppnm _ _ bd]) := do
       (++) (if bd.has_zero_var then [] else [ppnm]) <$>
        find_unused_have_macro bd
| (macro md l) := do ls ← l.mmap find_unused_have_macro, return ls.join
| _ := return []

meta def unused_of_decl : declaration → tactic (list name)
| (defn a a_1 a_2 bd a_4 a_5) := find_unused_have_macro bd
| (thm a a_1 a_2 bd) := find_unused_have_macro bd.get
| _ := return []

@[linter] meta def linter.unused_haves : linter :=
{ test := λ d,
  (do ns ← unused_of_decl d,
   if ns.length = 0 then return none else return (", ".intercalate (ns.map to_string))),
  no_errors_found := "all good",
  errors_found := "DECLS HAVE UNNEEDED HAVES",
  is_fast := tt,
  auto_decls := ff }

#lint only unused_haves

[Rob Lewis]

I'm tempted to run this on the assignments from my course this spring, but it might make me sad

[Rob Lewis]

(It doesn't catch tactic mode haves.)