just run one linter?

Stream: std4

[Kevin Buzzard]

How do I run one linter as opposed to #lint which runs all of them? I tried #lint only but I couldn't get it to work.

import Std.Tactic.Lint

structure MulOpposite (α : Type u) : Type u where
  /-- The element of `MulOpposite α` that represents `x : α`. -/ op ::
  /-- The element of `α` represented by `x : αᵐᵒᵖ`. -/ unop : α

/-- Multiplicative opposite of a type. -/
postfix:max "ᵐᵒᵖ" => MulOpposite

namespace MulOpposite

instance [Mul α] : Mul αᵐᵒᵖ where mul x y := op (unop y * unop x)

def SemiconjBy [Mul M] (a x y : M) : Prop :=
  a * x = y * a

@[simp]
theorem semiconj_by_unop [Mul α] {a x y : αᵐᵒᵖ} :
    SemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy a x y := sorry

end MulOpposite

#lint only simpComm -- docBlame linter reports

[Mario Carneiro]

The syntax for #lint looks a bit overambitious:

elab "#lint"
  project:(ident)?
  verbosity:("+" <|> "-")?
  fast:"*"?
  only:(&" only")?
  linters:(ppSpace ident)* : command

The project field is problematic because it overlaps with only (which is not a token and so is parsed like an identifier). So most likely what is happening in your example is that only is the project name, the only flag is not set, and simpComm is an explicit linter specification. (Notice that in the printout it says "found N errors in D declarations (...) in only with L linters".)

[Mario Carneiro]

I think the most sensible way to fix this is to make project use an option-like syntax such as #lint+* (project := my_proj) only simpComm