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).