Conversation
Found after examining the bug fixes in #12054, although these improvements are unrelated to the test PR.
PR summary a1b1d7792dImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
joneugster
left a comment
There was a problem hiding this comment.
Overall, I think this is a useful linter. I left a few comments on quesions I had.
Especially, I found it a bit hard to see immediately how to extend the linter with new tests and think some additional guidance to the unexperienced user might be useful.
One thing I cannot judge is whether everything in low_level_syntax belongs in other files.
| /-- | ||
| info: Skipped since it contains 'guard_target' | ||
|
|
||
| Use '#meta_test cmd' if you really want to run the test on 'cmd' | ||
| -/ | ||
| #guard_msgs in |
There was a problem hiding this comment.
I don't understand why this is in here. If I comment it, the test still passes, but commenting the set_option above suddenly makes this fail. Is there a reason for having the #guard_msgs duplicated?
| d.kind == .default && d.type.ctorName != "sort" && !(← inferType d.type).isProp | ||
| let toSet := nonSort.map Prod.snd | ||
| let (ntac, repls) ← addLetsOrSets lets? unLet? tac toSet | ||
| testTactic ntac m!"{if lets? then "'let's" else "'set's"} {repls}" m!"missing withContext? {ntac}" |
There was a problem hiding this comment.
Reading this as a non-expert it wasn't immediately obvious whether you mean "missing withContext?" or "missing withContext?" as it's not uncommon in Lean to add a ? to the name of things. same for instantiateMVars? below.
| /-- | ||
| warning: goal does not match | ||
| -/ | ||
| -- `goal does not match` --> not dealing with `mdata`? | ||
| #guard_msgs in |
There was a problem hiding this comment.
If I uncomment any of these #guard_msgs (basically any in this entire file) then suddenly the one above it fails. It looks like #meta_test is including too much. This seems like a bug, isn't it?
| section testing_internals | ||
| open Lean Elab Parser Command Mathlib Tactic MetaTesting | ||
|
|
||
| run_cmd liftTermElabM do | ||
| let stx ← `(tacticSeq| exact .intro) | ||
| let gh := stx.insertMany #[(← `(tactic| guard_hyp h))] | ||
| let gt := stx.insertMany #[(← `(tactic| guard_target = h))] | ||
| guard <| (test? stx).isNone && (test? gh).isSome && (test? gt).isSome | ||
|
|
||
| run_cmd liftTermElabM do | ||
| let stx ← `(command| /-- -/ #guard_msgs in import) | ||
| guard <| (test? stx).isNone | ||
| let stx ← `(command| #guard_msgs in import) | ||
| guard <| (test? stx).isNone | ||
|
|
||
| end testing_internals |
There was a problem hiding this comment.
Could you add a comment explaining what you are testing here?
| for test in [testMData, testFVs false false, testFVs true false, testInstMVs, | ||
| testFVs false true, testFVs true true | ||
| ] do |
There was a problem hiding this comment.
I wonder if it would be a little bit easier for future developers if this list of tests would be extracted in it's own definition or marked better in another way. That might help understanding quickly how one adds new tests to the linter. Maybe even add an instruction to the module docstring like "you can add new tests to activeMetaTests."
Maybe not, but I think I had to read through the code just a bit too long to understand.
| warning: missing withContext? | ||
|
|
||
| let _h : ?a✝ := _h | ||
| let _d : ?a✝¹ := _d | ||
| guard_target = _ | ||
| exact 0 | ||
| done | ||
| --- | ||
| warning: missing withContext? | ||
|
|
||
| let _h : ?a✝ := _h | ||
| let _d : ?a✝¹ := _d | ||
| unfold_let at * | ||
| guard_target = _ | ||
| exact 0 | ||
| done |
There was a problem hiding this comment.
Why is this message appearing (almost) duplicated? and what does it tell us, that exact has no withContext?
Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
…thlib4 into adomani/test_all
adomani
left a comment
There was a problem hiding this comment.
Jon, thank you for the review!
For the moment, I have simply committed the "style" changes. I will look at the more substantial comments that you left soon!
This PR introduces a linter for suggesting bugs in tactics.
See
for some bugs exposed by the test suite.