/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module
public import FormalConjecturesUtil.Attributes.Basic
public import Mathlib.Tactic.Lemma
public meta import Batteries.Data.Array.MergeThe AMS Linter
The AMSLinter is a linter to aid with formatting contributions to
the Formal Conjectures repository by ensuring that results in a file have
the appropriate subject tags.
public meta sectionopen Lean Elab Meta Linter Command Parser Term ProblemAttributesregister_option linter.style.ams_attribute : Bool := {
defValue := false
descr := "enable the `AMS` attribute style linter"
}namespace AMSLinter
Checks if a command has the AMS attribute.
def toAMS (stx : TSyntax ``Command.declModifiers) :
CommandElabM (Array <| TSyntaxArray `num) := do
match stx with
| `(declModifiers| $(_)? @[$[$atts],*] $(_)? $(_)? $(_)? $(_)?) =>
atts.filterMapM fun att ↦ do
match att with
| `(attrInstance | AMS $nums*) => return some nums
| _ => return none
| _ => return #[]def mkAMSSyntax (nums : TSyntaxArray `num) : CommandElabM <| TSyntax ``attrInstance := do
return ← `(attrInstance | AMS $nums*)
The problem category linter checks that every theorem/lemma/example
has been given an AMS attribute.
def AMSLinter : Linter where
run := withSetOptionIn fun stx => do
match stx with
| `(command| $a:declModifiers theorem $_ $_:bracketedBinder* : $_ := $_)
| `(command| $a:declModifiers lemma $_ $_:bracketedBinder* : $_ := $_)
| `(command| $a:declModifiers example $_:bracketedBinder* : $_ := $_) =>
let ams ← toAMS a
let outStx := match a with
| `(declModifiers| $(_)? $atts $(_)? $(_)? $(_)? $(_)?) => atts.raw
| _ => stx
if ams.size > 1 then
let numerals := ams.flatten
let outCorrect := m!"{← mkAMSSyntax numerals}"
let currentOut := m!", ".joinSep (← ams.mapM fun nums ↦ do return m!"{← mkAMSSyntax nums}").toList
logLintIf linter.style.ams_attribute outStx
m!"The AMS tag should be formatted as {outCorrect} rather than {currentOut}"
return
if ams.size == 0 then
logLintIf linter.style.ams_attribute outStx
"Missing AMS attribute."
return
if ams.flatten.isEmpty then
-- If we're here then there is at least one AMS tag, but it doesn't have any number.
logLintIf linter.style.ams_attribute outStx
"The AMS tag should have at least one subject number."
return
-- Avoid AMS tags with leading zeros (e.g. AMS 05 -> AMS 5)
for n in ams.flatten do
if let some str := n.raw.reprint then
let trimmed := str.trimAscii.toString
if trimmed.length > 1 && trimmed.startsWith "0" then
logLintIf linter.style.ams_attribute outStx
m!"AMS subject {trimmed} should not have a leading zero."
-- Check there the AMS tags are sorted and do not contain duplicates
let ams_sorted := ams.flatten.qsort (fun n m => n.getNat < m.getNat)
if ams_sorted != ams.flatten then
logLintIf linter.style.ams_attribute outStx
m!"The AMS tags should be ordered as {← mkAMSSyntax ams_sorted}"
return
if ams_sorted.dedupSorted != ams_sorted then
logLintIf linter.style.ams_attribute outStx
m!"AMS tags contain duplicates. This should be {← mkAMSSyntax ams_sorted.dedupSorted}"
| _ => returninitialize do
addLinter AMSLinterend AMSLinter