Many large-scale projects require custom linters that enforce project-specific standards.
The steps for defining a new linter are:
Registering an option to control the new linter.
Determining whether the linter should be a command linter, module linter, stateful linter, or environment linter.
Deciding which code quality metrics, if any, should be saved.
Implementing any package-level code quality checks that are needed.
The first step in defining a linter is to register the option that controls it.
Options are registered using Lean.Option.registerOption : commandregister_option, which takes a default value and a description for the new option.
The default value determines whether the linter is enabled or disabled by default.
In a module, this option should be both public and in the meta phase.
Linters should be controlled by a Bool option.
Further options that configure a linter, such as options that set thresholds, may be added within the linter's own namespace.
Linters should use logLint or Lean.Linter.logLintIf instead of Lean.logWarning to display lint warnings.
These helpers ensure that the linter warning's message is formatted consistently.
They also internally tag it as a linter message, which causes Lake and Lean to include it in lake lint's output.
logLintIf additionally resolves the linter option's value correctly, taking linter.all and linter sets into consideration.
logLint should be used in contexts where the linter's option has already been checked.
Some linters need to check whether they are enabled before they are ready to log a warning.
For example, computationally expensive linters that do not compute any useful code quality metrics may wish to terminate early if they are not enabled.
These linters should check whether they are enabled using helpers that correctly take linter sets and linter.all into account.
This is done by first calling Lean.Linter.getLinterOptions, and then checking the option's value using Lean.Linter.getLinterValue.
Finally, the implementation of each linter should wrap command-specific checks with Lean.withSetOptionIn.
Without this wrapper, uses of Lean.Parser.Command.set_option : command`set_option <id> <value>` sets the option `<id>` to `<value>`. Depending on the type of the option,
the value can be `true`, `false`, a string, or a numeral. Options are used to configure behavior of
Lean as well as user-defined extensions. The setting is active until the end of the current `section`
or `namespace` or the end of the file.
Auto-completion is available for `<id>` to list available options.
`set_option <id> <value> in <command>` sets the option for just a single command:
```
set_option pp.all true in
#check 1 + 1
```
Similarly, `set_option <id> <value> in` can also be used inside terms and tactics to set an option
only in a single term or tactic.
set_option...Lean.Parser.Command.in : commandin ... around the command being linted are not taken into account.
Command linters and stateful linters should wrap it around their entire implementation, while module linters should wrap operations on single commands.
If linterOption is enabled, print a linter warning message at the position determined by stx.
Whether a linter option is enabled or not is determined by the following sequence:
If it is set, then the value determines whether or not it is enabled.
Otherwise, if linter.all is set, then its value determines whether or not the option is enabled.
Otherwise, if any of the linter sets containing the option is enabled, it is enabled.
(Only enabled linter sets are considered: explicitly disabling a linter set
will revert the linters it contains to their default behavior.)
Otherwise, the default value determines whether or not it is enabled.
Given a function cmd on command syntax, returns a new function that
first peels off and evaluates set_option...in... syntax recursively, updating the options
accordingly, and then invokes cmd on the inner syntax. The result type is arbitrary, so that
besides CommandElabs this can also wrap functions that return values, such as the phases of a
stateful linter.
This is expected to be used in linters, after elaboration is complete. It is not appropriate for
ordinary elaboration of outer set_options, since it
does not update the infotrees with info for the set_option commands
silently ignores failures in setting the given options (e.g. we do not error if the option is
unknown or the wrong type of value is provided), as these should have been reported during
original elaboration.
Command linters are the simplest form of linter.
A command linter is a value of type Lean.Elab.Command.Linter, which is a structure with a run field of type Syntax→CommandElabMUnit.
The addLinter function saves a new command linter, and must be run in an Lean.Parser.Command.initialize : commandinitialize block.
The Lean.Parser.Command.initialize : commandinitialize block must be in the meta phase when used in a module.
Command linters are run after the elaboration of each command, concurrently with the elaboration of the rest of the file.
The linter's run function is applied to the command's syntax in a context where the command's info tree is available.
Any environment modifications made by the linter are discarded, but new message log entries, code actions, and code quality metrics are saved.
This custom linter issues a warning when the number of tactics in a command exceeds a configurable threshold.
Tactics are found by processing the command's info tree, recording the unique starting positions of original syntax with tactic info whose kind is a tactic kind.
Deduplication is needed because tactic info is saved for macro expansion steps and repeated executions of the same tactic.
The linter terminates early if it is disabled, rather than waiting until it is time to log the message to make the decision.
Steps/Linter.leanmodulepublicmetaimportLean.Linter.BasicpublicmetaimportLean.Elab.InfoTree.UtilopenLeanElabCommandopenStd(HashSet)metasectionpublicregister_optionlinter.tacticCount:Bool:={defValue:=truedescr:="warn when a command runs many tactics"}publicregister_optionlinter.tacticCount.max:Nat:={defValue:=100descr:="the number of tactics a command may run before \
`linter.tacticCount` warns"}openParserin/--
Whether `kind` is the syntax kind of a tactic, as opposed to a tactic
sequence or block.
-/defisTacticKind(env:Environment)(kind:SyntaxNodeKind):Bool:=match(parserExtension.getStateenv).categories.find?`tacticwith|somecategory=>category.kinds.containskind|none=>false/--
The number of distinct tactics from the source file that were run while
elaborating `tree`.
-/defcountTactics(env:Environment)(tree:InfoTree):Nat:=letpositions:HashSetString.Pos.Raw:=tree.foldInfo(init:={})fun_infopositions=>matchinfowith|.ofTacticInfoti=>matchti.stx.getHeadInfo,ti.stx.getPos?with|.original..,somepos=>ifisTacticKindenvti.stx.getKindthenpositions.insertposelsepositions|_,_=>positions|_=>positionspositions.sizeopenLinterin/--
Warns when a command runs more than `linter.tacticCount.max` tactics.
-/deftacticCount:Linterwhererun:=withSetOptionInfunstx=>do-- Don't compute the result if it will never be shownunlessgetLinterValuelinter.tacticCount(←getLinterOptions)doreturnletenv←getEnvletcount:=(←getInfoState).trees.foldl(init:=0)funnt=>n+countTacticsenvtletlimit:=linter.tacticCount.max.get(←getOptions)ifcount>limitthenLinter.logLintlinter.tacticCountstxm!"this command runs \
{count} tactics, more than {limit}"initializeaddLintertacticCount
This module demonstrates that the linter runs and that it respects locally set options:
Steps/Test.leanmoduleimportSteps.Linterset_optionlinter.tacticCount.max4theoremshort(n:Nat):n+0=n:=n:Nat⊢ n+0=nAll goals completed! 🐙this command runs 5 tactics, more than 4Note: This linter can be disabled with `set_option linter.tacticCount false`theoremlong(ab:Nat):a+b=b+a:=a:Natb:Nat⊢ a+b=b+ainductionawithb:Nat⊢ 0+b=b+0All goals completed! 🐙b:Nata:Natih:a+b=b+a⊢ a+1+b=b+(a+1)b:Nata:Natih:a+b=b+a⊢ (a+b).succ=b+(a+1)b:Nata:Natih:a+b=b+a⊢ (b+a).succ=b+(a+1)All goals completed! 🐙set_optionlinter.tacticCountfalseintheoremsilenced(ab:Nat):a+b=b+a:=a:Natb:Nat⊢ a+b=b+ainductionawithb:Nat⊢ 0+b=b+0All goals completed! 🐙b:Nata:Natih:a+b=b+a⊢ a+1+b=b+(a+1)b:Nata:Natih:a+b=b+a⊢ (a+b).succ=b+(a+1)b:Nata:Natih:a+b=b+a⊢ (b+a).succ=b+(a+1)All goals completed! 🐙
this command runs 5 tactics, more than 4Note: This linter can be disabled with `set_option linter.tacticCount false`
Module linters run after each module's elaboration is completed.
Module linters have type Lean.Elab.Command.ModuleLinter, which is a structure with a run function of type ArraySyntax→CommandElabMUnit.
The function is called on all the top-level commands from the module.
Because the linter is invoked after the whole module is elaborated, its warnings do not appear until the very end of elaboration.
Unlike command linters, module linters do not have access to the commands' info trees and cannot save code actions.
They do, however, have access to the module's final environment.
This means that they are primarily useful for syntactic checks.
If info trees are needed for a whole-file check, consider using a stateful linter instead.
The addModuleLinter function saves a new module linter, and must be run in an Lean.Parser.Command.initialize : commandinitialize block.
The Lean.Parser.Command.initialize : commandinitialize block must be in the meta phase when used in a module.
The module Limit.Linter contains a module linter that issues a warning when a module contains too many declarations.
The limit is determined by the value of an option.
Even though the warning is attached to the first declaration that exceeds the limit, it does not appear until the entire file is elaborated because it is implemented as a module linter.
Limit/Linter.leanmodulepublicmetaimportLean.Linter.BasicopenLeanElabCommandmetasectionpublicregister_optionlinter.declarationLimit:Bool:={defValue:=truedescr:="warn when a file contains more declarations than \
`linter.declarationLimit.max`"}publicregister_optionlinter.declarationLimit.max:Nat:={defValue:=200descr:="the number of declarations that a file may contain"}/-- Warns at the first declaration past the limit. -/defdeclarationLimit:ModuleLinterwhereruncmds:=doletlimit:=linter.declarationLimit.max.get(←getOptions)letdecls:=cmds.filter(·.isOfKind``Parser.Command.declaration)ifh:limit<decls.sizethenLinter.logLintIflinter.declarationLimitdecls[limit]m!"this file contains {decls.size} declarations, more than \
{limit}"initializeaddModuleLinterdeclarationLimit
This module sets the maximum declaration count to 2:
Limit/Test.leanmoduleimportLimit.Linterset_optionlinter.declarationLimit.max2defa:=1defb:=2this file contains 3 declarations, more than 2Note: This linter can be disabled with `set_option linter.declarationLimit false`defc:=3
Building the file demonstrates the linter warning:
this file contains 3 declarations, more than 2Note: This linter can be disabled with `set_option linter.declarationLimit false`
Like command linters, stateful linters are invoked after each command is elaborated.
Similarly, they also have access to the command's info tree and environment.
Unlike command linters, they are not independent of the results of linting prior commands.
Instead, they have a state that is accumulated throughout the module.
This provides the opportunity to check non-local properties, while still emitting a warning as soon as the violation has occurred rather than waiting for the rest of the file to be processed.
Furthermore, stateful linters are run in two phases, called the “early” and “late” phases.
After command elaboration is complete, the early phases of all stateful linters are run, followed by all late phases.
This allows cooperation: an early phase might compute data that is used in the late phases of multiple linters.
The early phase is optional, and many useful stateful linters have no early phase.
Stateful linters may read the saved state of any other stateful linter, not just their own, via handles returned by linter registration.
Stateful linters are registered using Lean.Elab.Command.registerStatefulLinter.
Like the other linter registration functions, it must be invoked in an Lean.Parser.Command.initialize : commandinitialize block in the meta phase.
The linter must be public.
The registration function takes the implementations of the early and late phases as arguments.
Unlike the other linter registrations, registration returns a useful value; this value is a handle by which the linter's state can be read.
StatefulLinter and registerStatefulLinter both take two type parameters; the first is the state that is threaded between commands, the second is the data computed in the early phase.
Stateful linters are also run at the end of the module.
Because they've had the opportunity to collect information from each command, they can provide feedback that module linters cannot.
Registers a stateful linter and returns its handle (used by other linters to read its state).
Must be called during initialization.
Lifecycle Phases
pre: Reads the previous command's persistant state (via readPrevPostState)
and optionally outputs a pre-phase state (type Optionτ).
post: Reads the previous command's state and all current pre-phase outputs
(via readPrevPostState and readCurrentPreState), then produces the new state (type σ)
for the next command.
State Access Rules
Self: Access its own persistent and pre-phase states directly via selfPrevPostState and
selfCurrentPreState.
Others: Access other linters' states only via the readPrevPostState and
readCurrentPreState closures that take typed handles of other linters.
This stateful linter checks that a module has a particular structure.
It should start with a module docstring, then set any options that are needed, and then finally include declarations.
The linter's state is a simple state machine that tracks this ordering.
When it encounters a command, it checks the invariant locally and updates the state.
This file contains three violations: it begins without a module documentation comment, it sets an option after a declaration, and it places a module documentation comment after a command:
Layout/Test.leanmoduleimportLayout.Linterthe first command in a file should be a module docstringNote: This linter can be disabled with `set_option linter.fileLayout false`openNatmodule docstring after setup commandNote: This linter can be disabled with `set_option linter.fileLayout false`/-! This module docstring comes too late. -/defx:=1setup command after declarationNote: This linter can be disabled with `set_option linter.fileLayout false`set_optionautoImplicitfalsetheoremy:x=1:=rfl
the first command in a file should be a module docstringNote: This linter can be disabled with `set_option linter.fileLayout false`
setup command after declarationNote: This linter can be disabled with `set_option linter.fileLayout false`
module docstring after setup commandNote: This linter can be disabled with `set_option linter.fileLayout false`
Environment linters are run by lake lint after a project is built when --builtin-lint is enabled or the builtinLint field is enabled in the Lake configuration.
After Lake builds the project, its built-in linter iterates over each library target's root module, importing the module and then running the configured environment linters on the resulting environment.
Each environment linter consists of a test routine along with success and failure messages.
Unlike command and module linters, environment linters do not need to be transitively imported by the modules that they check.
Like other linters, environment linters are controlled by options.
Unlike the linter itself, the option declaration must be transitively imported.
Options that control environment linters are specially registered, and the values of these options are stored during elaboration so that the linter can retrieve the option values from the imported environment, even those that are locally set using Lean.Parser.Command.in : commandin.
To define an environment linter, do the following:
In one module, register a public option in the meta phase that controls the linter.
In an Lean.Parser.Command.initialize : commandinitialize block, run addEnvLinterOption to instruct Lean to track the option's value during elaboration.
This module should be transitively imported by every module in which the linter is to be used.
The initialize block must run in the meta phase.
In a second module, define the linter itself.
Use the Lean.Linter.EnvLinter.builtin_env_linter : attrDefines the `builtin_env_linter` attribute for registering an environment linter.
Each environment linter needs to have a registered Boolean-value `Lean.Option` that will be
associated with it by providing the option name in the attribute, i.e.
`@[builtin_env_linter linter.envLinter.myLinter]`.
builtin_env_linter attribute to associate the linter with the option.
This module does not need to be imported by a module in order to check it, but it must be transitively imported by the root module of the target being linted.
attributeEnvironment Linters
attr::= ...
|Defines the `builtin_env_linter` attribute for registering an environment linter.
Each environment linter needs to have a registered Boolean-value `Lean.Option` that will be
associated with it by providing the option name in the attribute, i.e.
`@[builtin_env_linter linter.envLinter.myLinter]`.
builtin_env_linterident
Registers an environment linter that is controlled by the indicated option name.
test : Lean.Name→Lean.MetaM(OptionLean.MessageData)
test defines a test to perform on every declaration. It should never fail. Returning none
signifies a passing test. Returning somemsg reports a failing test with error msg.
noErrorsFound : Lean.MessageData
noErrorsFound is the message printed when all tests are negative
errorsFound : Lean.MessageData
errorsFound is printed when at least one test is positive
Generally speaking, a data structure that provides a get! function should also provide get? and getD.
These functions need not be defined in the same module, however.
An environment linter can ensure that every namespace in a project that defines any of these names also defines the others.
The linter itself consists of two modules: Lints.Options defines the option that controls the linter and should be imported by the entire project, while Lints.GetVariants only needs to be imported by the root module:
modulepublicmetaimportLean.Linter.InitopenLeanmetasectionpublicregister_optionlinter.envLinter.getVariants:Bool:={defValue:=truedescr:="warn when a namespace defines some but not all of `get!`, \
`get?`, and `getD`"}initializeLinter.addEnvLinterOptionlinter.envLinter.getVariantsmodulepublicimportLints.OptionspublicmetaimportLean.Linter.EnvLinter.BasicopenLeanLinterEnvLintermetasection/-- The variants that are expected to be defined together. -/defgetVariants:ListString:=["get!","get?","getD"]@[builtin_env_linterlinter.envLinter.getVariants]publicdefgetVariantsLinter:EnvLinterwheretestdeclName:=dolet.strnsvariant:=declName|returnnoneunlessgetVariants.containsvariantdoreturnnoneletenv←getEnvletmissing:=getVariants.filterfunv=>!env.contains(.strnsv)ifmissing.isEmptythenreturnnoneletmissing:=missing.mapfunv=>m!"`{Name.strnsv}`"returnsomem!"`{declName}` is defined, but \
{MessageData.andListmissing} \
{ifmissing.length==1then"is"else"are"} not"noErrorsFound:="Every namespace defines all of `get!`, `get?`, and \
`getD`."errorsFound:="THE FOLLOWING NAMESPACES DEFINE ONLY SOME OF `get!`, \
`get?`, AND `getD`:"
The library itself contains a variety of data structures, with their implementations in multiple modules:
Linting the package returns the following warnings:
$ lake lint --builtin-only
-- Found 1 error in 12 declarations (plus 24 automatically generated ones) in Data with 1 linters
/- The `linter.envLinter.getVariants` linter reports:
THE FOLLOWING NAMESPACES DEFINE ONLY SOME OF `get!`, `get?`, AND `getD`: -/
-- Data.Queue
./Data/Queue.lean:7:1: error: Queue.get! `Queue.get!` is defined, but `Queue.get?` and `Queue.getD` are not
Code quality entries relate a metric name, a source, and a value.
The metric name may be any string, but to avoid overlap, it should typically include the linter's option name as a prefix.
Using only the linter's name risks conflicting with the automatic counts of linter warnings that Lake emits as code quality metrics.
The helpers Lean.Linter.findCodeQualitySource and Lean.Linter.findCodeQualitySource? determine a Source from syntax parsed from the file, with the former falling back to the current module if it cannot find a declaration.
Sources may only be modules or declarations, and there is no way to attribute an entry to a smaller unit.
Instead, dictionary values can be used that encode the finer structure.
Values may be floating-point values or dictionaries that map strings to floating-point numbers.
Integral measures, such as counts, should also use floating-point numbers.
The same metric name may be logged any number of times for a given source.
Clients are responsible for aggregating metrics appropriately.
Records the code quality entry e into codeQualityLogExt so that it is persisted into the
.olean and can be recovered by consumers via getAllCodeQualityEntries.
This can be safely used in Linters. While regular Lean.Linters, module linters, and stateful
linters all have their environment changes discarded after running, entries they log are
captured per command (see Command.State.codeQualityEntryTasks) and merged into the final
environment in runFrontend.
The entry is recorded without a linter attribution, so it is recorded unconditionally and no
linter selection flag (e.g. lake lint --lint-only) can suppress it. Inside a linter guarded by
an option, use logCodeQualityEntryIf instead; this variant is meant for unconditional metrics
not tied to any linter option.
Similar to logLintIf, but for logCodeQualityEntry - i.e. it logs an entry only if the
provided linter option is enabled, taking linter.all and linter sets into account. The entry
is recorded with linterOption.name as its attribution, so consumers can filter it by linter
selection (e.g. lake lint --lint-only).
Find the declaration in the current file that stx belongs to.
Searches the info trees of the current command for declarations (see getNewDecls) whose
declaration range contains the range of stx, and returns the one whose range starts earliest.
Returns none if stx has no position or no declaration's range contains it (e.g. for commands
such as #check or open).
Build a code-quality Source attributing stx to the declaration it belongs to
(see findMatchingDecl?), falling back to the current module if no declaration matches.
Build a code-quality Source attributing stx to the declaration it belongs to
(see findMatchingDecl?), or none if no declaration matches.
Measuring Simp Lemma Usage
Even though linters are primarily intended to warn about potentially problematic code, they can also be used to just gather metrics, with warnings emitted by later checks.
This example demonstrates a command linter that logs metrics about the usage of explicit simp lemmas, which could provide insights into missing @[simp] annotations in a library.
These metrics are then collected and summarized by a small Lean program.
The linter first traverses the syntax of the command with simpLemmaStarts, which finds the source location of each explicit simp lemma.
Lemmas are identified by their starting position because a simp lemma list allows the lemmas to be applied to arguments.
The simpUsage linter itself then uses the info tree to discover constant references that begin at the identified starting positions, logging a metric that contains a dictionary that maps fully-resolved names to occurrence counts.
This script takes the collected metrics from a project and summarizes them.
The function parseEntries parses a sequence of JSON values, while main processes the result and sorts the simp lemmas by their usage count.
importLean.Data.JsonopenLean/--
Parses a sequence of JSON values, as printed by
`lake lint --code-quality`.
-/defparseEntries(s:String):ExceptString(ArrayJson):=letp:Std.Internal.Parsec.String.Parser(ArrayJson):=doStd.Internal.Parsec.String.wsletentries←Std.Internal.Parsec.manyJson.Parser.anyCoreStd.Internal.Parsec.eofreturnentriesp.runsdefmain:IOUInt32:=doletinput←(←IO.getStdin).readToEndletentries←IO.ofExcept(parseEntriesinput)letmuttotals:Std.TreeMapStringFloat:={}forentryinentriesdolet.ok"linter.simpUsage.lemmas":=entry.getObjValAs?String"name"|continuelet.ok(.objdict):=doletv←entry.getObjVal?"value"letd←v.getObjVal?"dict"d.getObjVal?"dictionary"|continuefor(lemma,count)indictdolet.okn:=count.getNum?|continuetotals:=totals.insertlemma(totals.getDlemma0+n.toFloat)letsorted:=totals.toArray.qsortfun(_,a)(_,b)=>a>bfor(lemma,n)insorteddoIO.printlns!"{n.toUInt64} {lemma}"return0
The project itself contains four lemmas, t1 through t4, spread across two modules:
Package code quality checks are an opportunity to measure a property of an entire library or executable target, as opposed to a declaration or module in isolation.
They are configured in the Lake configuration file or on the command line, and do not need to be imported by the code that they are measuring.
Package checks emit code quality entries.
Because they run as part of Lean and Lake, they have access to Lean's metaprogramming features and do not need to build their own ad hoc mechanisms.
Scripts that enforce a limit or invariant on a whole package only need to parse JSON, rather than interacting with Lean code in complicated ways.
Package checks are enabled by adding their defining modules to the checks field in the Lake configuration or by using Lake's --checks option.
Within the configured package check modules, each check is a public definition of type PackageCheck in the meta phase that is registered with the package_code_quality_check attribute.
Given an argument of type PackageCheckContext, a package check may use any feature of MetaM to compute an array of code quality entries.
The context specifies the library or executable's root module along with the workspace's source search path.
Package checks should not throw exceptions to indicate that the package violated an invariant or desired property; instead, these issues should be returned as entries and then checked by a consumer of the data.
Enabled checks are run only when the --code-quality or --checks options are passed—lake lint will not otherwise run them.
For each root module, all registered package checks are run concurrently, and their resulting entries are appended to the overall collection of quality metrics.
Modules that are included in libraries through their globs field are not considered as roots.
Custom targets are not included, even if they build Lean code, and neither are non-default library and executable targets.
If modules are specified on the command line, they are checked instead of the default targets' root modules.
Exceptions thrown by package checks are written to standard error, but do not terminate linting.
If any exceptions were thrown, lake lint returns a non-zero exit code.
Checks are run in an environment in which the root module is imported.
Modules that are imported by multiple root modules can be checked multiple times by package checks.
If the root module is a module using the module system, then only public and server information is available in this environment; private declarations are not visible.
If the root module does not use the module system, then private information is also visible.
Each root module is checked in a fresh environment.
Because package checks have access to an entire library, they can be used to find duplicate theorems.
This example check is limited: it only finds theorems that match each other almost exactly, and does not take reorderings of hypotheses or unfoldings of definitions into account.
A more realistic check could use a more nuanced similarity measure, reporting theorems that exceed some threshold measure.
First, the Checks module is added to the package's checks field:
Its single check starts by computing equivalence classes of theorems.
Theorems are identified by checking whether their types are propositions, and internal theorems produced as helpers for other declarations are skipped.
Non-internal theorems are sorted into equivalence classes using a hash table; the BEq instance for Lean.Expr and its corresponding HashableLean.Expr instance check equality modulo renaming of bound variables and changes of binder info.
Only modules in the root module's package are searched.
As a result, theorems that differ only by hypothesis naming or status as implicit parameters are grouped, while those that re-order hypotheses are not.
After the equivalence classes are identified, each element of each class with more than one element is given a metrics entry that lists the entire class.
modulepublicmetaimportLean.Linter.CodeQuality.FrontendpublicmetaimportLean.Compiler.ModPkgExtopenLeanMetaLinterCodeQualitymetasection@[package_code_quality_check]publicdefduplicateTheorems:PackageCheckwhererunctx:=doletenv←getEnvletsomerootIdx:=env.getModuleIdx?ctx.topLevelModule|return#[]letpkg:=env.getModulePackageByIdx?rootIdx-- Group the theorems of the package's modules by their statements.-- Each equivalence class is a dictionary that maps its members'-- names to 1.0 to facilitate reporting.letmutclasses:ExprMap(Std.TreeMapStringFloat):={}letmuttheorems:=#[]forh:iin0...env.header.moduleData.sizedounlessenv.getModulePackageByIdx?i==pkgdocontinuefordeclNameinenv.header.moduleData[i].constNamesdoifdeclName.isInternalDetailthencontinueletsomeinfo:=env.find?declName|continueunless←isPropinfo.typedocontinueclasses:=classes.alterinfo.typefundups?=>some((dups?.getD{}).insertdeclName.toString1.0)letmodName:=env.header.moduleNames[i]!theorems:=theorems.push(modName,declName,info.type)-- Report each theorem that has duplicates.letmutentries:=#[]for(modName,declName,type)intheoremsdoletsomedups:=classes[type]?|continueifdups.size<2thencontinueentries:=entries.push{name:="duplicateTheorems"source:=.declarationmodNamedeclNamevalue:=.dictdups}returnentries
The code itself contains multiple restatements of the same theorem, three of which fall into the same equivalence class.
zero_add' and add_zero_rev have different statements.
