Checking which axioms are used in a project

Stream: general

[Riccardo Brasca]

Is there a linter or something similar to check that an axioms is not used in a whole project? By this I mean that if I run #print axioms foo for all foo in the project then axiom bar is not shown.

For a little of context, bar is Classical.choice, and, in the case it matters, the project actually contains one specific axiom. If you are curious I am working on Synthetic Differential Geometry, a theory that is "anticlassical" (I know Lean + mathlib is probably not the best proof assistant for this, but I am curious to see if something nontrivial can be done) and so I need to be sure that choice is never used.

[Damiano Testa]

I did not use this in a while, but there used to be #lean4 > restricting axioms @ 💬.

[Sebastian Ullrich]

nanoda has an option for that: https://github.com/ammkrn/nanoda_lib?tab=readme-ov-file#configuration-options:~:text=The%20%22permitted_axioms%22%20list%20is%20where%20users%20specify%20the%20axioms%20an%20export%20file%20is%20permitted%20to%20use.

[Riccardo Brasca]

Thanks! Learning how to use an external checker seems more complicated than checking the last declaration by hand (hoping it uses everything...), but it's very nice that is doable.

[Riccardo Brasca]

@Damiano Testa of course being a couple of moths old your code does not work anymore. Do you mind to have a look? It is probable simple to fix it (I am trying, but my metaprogramming skills are very limited)

[Damiano Testa]

I'll take a look right now!

[Riccardo Brasca]

ah, maybe it is enough to use Linter.getLinterOptions.

[Riccardo Brasca]

Yes, it works now, thanks!

[Damiano Testa]

Great, I was going to mention that as well!

[Damiano Testa]

I also updated the code snippet in the other thread.

[Riccardo Brasca]

In case someone else is interested, it's enough to add weak.linter.verbose.detectClassical = true to the [leanOptions] section of lakefile.toml and the linter works perfectly. (In my case I modified it to not say anything on declaration that don't depend on choice).

[Riccardo Brasca]

@Damiano Testa do you have an idea on how to make this work using the new module system? Currently, I am using this version

/-
This file has been written essentially ba Damiano Testa.
-/
module

public meta import Lean.Util.CollectAxioms
public meta import Mathlib.Tactic.DeclarationNames
public meta import Mathlib.Init

/-!
#  The "detectClassical" linter

The "detectClassical" linter emits a warning on declarations that depend on the `Classical.choice`
and/or `sorryAx`.
-/

public meta section

open Lean Elab Linter Command

namespace Mathlib.Linter

/--
The "detectClassical" linter emits a warning on declarations that depend on the `Classical.choice`
axiom.
-/
register_option linter.detectClassical : Bool := {
  defValue := true
  descr := "enable the detectClassical linter"
}

namespace DetectClassical

@[inherit_doc Mathlib.Linter.linter.detectClassical]
def detectClassicalLinter : Linter where run := withSetOptionIn fun stx ↦ do
  unless Linter.getLinterValue linter.detectClassical (← getLinterOptions) do
    return
  if (← get).messages.hasErrors then
    return
  let nms := (← getNamesFrom (stx.getPos?.getD default)).filter (! ·.getId.isInternal)
  for constStx in nms do
    let constName := constStx.getId
    let axioms ← collectAxioms constName
    if !axioms.contains `Classical.choice && !axioms.contains `sorryAx then return
    else
      if !axioms.contains `Classical.choice then
        Linter.logLint linter.detectClassical constStx m!"'{constName}' depends on 'sorry'.\n"
      else
      if !axioms.contains `sorryAx then
        Linter.logLint linter.detectClassical constStx m!"'{constName}' depends on 'choice'.\n"
      else Linter.logLint linter.detectClassical constStx m!"'{constName}' depends on
        'sorry and choice'.\n"

initialize addLinter detectClassicalLinter

end DetectClassical

end Mathlib.Linter

but it seems to only understand sorryAx. Indeed I inspected axioms in a random declaration that depends on the axiom of choice because of grind but Classical.choice doesn't show up. Note that I know it depends on choice since if I do

#print axiom foo

in a file that is not a module I see the axiom (in a module #print axioms doesn't work at all :frown: ).

[Damiano Testa]

I do not know how to access axiom information from a module. The lnter seems to work on non-modules, though, right?

[Damiano Testa]

I suspect that the reason this is not working on modules is the same reason why #print axioms also does not work with the module system.

[Riccardo Brasca]

OK, I will just use it in a non-module. Thanks!

[Riccardo Brasca]

Another related question: @Damiano Testa do you think is it possible to count how many declarations depend on the axiom of choice in the current environment? I would like to have this number for mathlib and I don't care if it takes a couple of hours (or even a day, but if it takes one month it is a little slow).

[Paul Lezeau]

That seems very doable! I’m not at my computer now but I can send a script to do that as soon as I’m back:)

[Riccardo Brasca]

Thanks!

[Paul Lezeau]

This should do the trick:

import Mathlib

open Lean

run_cmd do
  let env ← getEnv
  let mut count := 0
  for (constName, _) in env.constants do
    let axioms ← collectAxioms constName
    if axioms.contains `Classical.choice then count := count + 1
  Lean.logInfo m!"Found {count} constants depending on Classical.choice"

[Riccardo Brasca]

Thanks! Let me test it with a very light import to see how long does it take.

[Robin Arnez]

This might be a bit more reasonable in terms of performance:

import Mathlib

open Lean
structure State where
  visited : NameMap Bool := {}

abbrev M := ReaderT Environment <| StateM (NameMap Bool)

partial def collect (c : Name) : M Bool := do
  let collectExpr (e : Expr) : M Bool := e.getUsedConstants.anyM collect
  let s ← get
  if let some res := s.find? c then
    return res
  let env ← read
  modify fun s => s.insert c false
  let res ← match env.checked.get.find? c with
  | some (ConstantInfo.axiomInfo v)  => collectExpr v.type
  | some (ConstantInfo.defnInfo v)   => collectExpr v.type <||> collectExpr v.value
  | some (ConstantInfo.thmInfo v)    => collectExpr v.type <||> collectExpr v.value
  | some (ConstantInfo.opaqueInfo v) => collectExpr v.type <||> collectExpr v.value
  | some (ConstantInfo.quotInfo _)   => pure false
  | some (ConstantInfo.ctorInfo v)   => collectExpr v.type
  | some (ConstantInfo.recInfo v)    => collectExpr v.type
  | some (ConstantInfo.inductInfo v) => collectExpr v.type <||> v.ctors.anyM collect
  | none                             => pure false
  modify fun s => s.insert c res
  return res

partial def collectAll : M Nat := do
  modify fun s => s.insert ``Classical.choice true
  let env ← read
  let mut count := 0
  for (constName, _) in env.constants do
    let hasChoice ← collect constName
    if hasChoice then count := count + 1
  return count

run_cmd do
  let env ← getEnv
  let count := collectAll.run env |>.run' {}
  Lean.logInfo m!"Found {count} constants depending on Classical.choice"

[Riccardo Brasca]

Oh yes, the other one is still running and this has already finished!

[Riccardo Brasca]

(on a light import)

[Riccardo Brasca]

It seems we have 386779 declaration that depend on choice, and 707013 in total (this gives a little less than 55%).

It's exactly what I wanted, thanks!