Zulip Chat Archive

I think it would be useful to have a list of all declarations in LTE that are currently not in the dependency tree of thm95.
I've done a fair amount of refactoring, and I think there's quite a lot of old code that can now be removed. Of course we can prune the system manually, but if someone wants to automate generating this list, that would be cool.
(We should probably still manually do the actual deletion, because some things on the list might actually be useful in the future.)

Alex J. Best (Apr 28 2021 at 23:13):

@Simon Hudon added a tactic to mathlib for doing precisely this.
If you import tactic.unused_decls and add @[main_declaration] to the theorem you want and then call #list_unused_decls [] below it finds all the unused decls in the current file. Assuming you want all of them you can add

#list_unused_decls ["src/breen_deligne/category.lean","src/breen_deligne/constants.lean","src/breen_deligne/eg.lean","src/breen_deligne/functorial_map.lean","src/breen_deligne/suitable.lean","src/breen_deligne/universal_map.lean","src/combinatorial_lemma.lean","src/facts/default.lean","src/facts/int.lean","src/facts/nnreal.lean","src/facts/normed_group.lean","src/for_mathlib/additive_functor.lean","src/for_mathlib/add_monoid_hom.lean","src/for_mathlib/arrow.lean","src/for_mathlib/big_operators_basic.lean","src/for_mathlib/category.lean","src/for_mathlib/curry.lean","src/for_mathlib/dfinsupp.lean","src/for_mathlib/equalizers.lean","src/for_mathlib/extend_from_nat.lean","src/for_mathlib/filter_at_top_bot.lean","src/for_mathlib/finsupp.lean","src/for_mathlib/Fintype/basic.lean","src/for_mathlib/free_abelian_group.lean","src/for_mathlib/Gordan.lean","src/for_mathlib/grading.lean","src/for_mathlib/grading_examples.lean","src/for_mathlib/grading_monoid_algebra.lean","src/for_mathlib/int_grading_lemma.lean","src/for_mathlib/kronecker.lean","src/for_mathlib/linear_algebra.lean","src/for_mathlib/nnreal.lean","src/for_mathlib/normed_group.lean","src/for_mathlib/normed_group_hom.lean","src/for_mathlib/normed_group_hom_bound_by.lean","src/for_mathlib/normed_group_hom_completion.lean","src/for_mathlib/normed_group_hom_equalizer.lean","src/for_mathlib/normed_group_quotient.lean","src/for_mathlib/order_basic.lean","src/for_mathlib/pi_nat_apply.lean","src/for_mathlib/preadditive_category.lean","src/for_mathlib/Profinite/basic.lean","src/for_mathlib/Profinite/functorial_limit.lean","src/for_mathlib/Profinite/limits.lean","src/for_mathlib/Profinite/locally_constant.lean","src/for_mathlib/Profinite/nhds.lean","src/for_mathlib/Profinite.lean","src/for_mathlib/pseudo_metric.lean","src/for_mathlib/quotient_group.lean","src/for_mathlib/real_Inf.lean","src/for_mathlib/simplicial/augmented.lean","src/for_mathlib/simplicial/complex.lean","src/for_mathlib/specific_limit.lean","src/for_mathlib/Top/limits.lean","src/for_mathlib/tsum.lean","src/for_mathlib/uniform_space_cauchy.lean","src/hacks_and_tricks/by_exactI_hack.lean","src/hacks_and_tricks/type_pow.lean","src/lem97.lean","src/liquid.lean","src/locally_constant/analysis.lean","src/locally_constant/NormedGroup.lean","src/locally_constant/Vhat.lean","src/Mbar/basic.lean","src/Mbar/bounded.lean","src/Mbar/Mbar_le.lean","src/Mbar/pseudo_normed_group.lean","src/normed_group/controlled_exactness.lean","src/normed_group/NormedGroup.lean","src/normed_group/normed_with_aut.lean","src/normed_group/pseudo_normed_group.lean","src/normed_snake.lean","src/normed_spectral.lean","src/partition.lean","src/polyhedral_lattice/basic.lean","src/polyhedral_lattice/category.lean","src/polyhedral_lattice/cech.lean","src/polyhedral_lattice/cosimplicial.lean","src/polyhedral_lattice/direct_sum.lean","src/polyhedral_lattice/finsupp.lean","src/polyhedral_lattice/Hom.lean","src/polyhedral_lattice/int.lean","src/polyhedral_lattice/pseudo_normed_group.lean","src/polyhedral_lattice/topology.lean","src/prop_92.lean","src/pseudo_normed_group/basic.lean","src/pseudo_normed_group/breen_deligne.lean","src/pseudo_normed_group/category.lean","src/pseudo_normed_group/CLC.lean","src/pseudo_normed_group/FiltrationPow.lean","src/pseudo_normed_group/homotopy.lean","src/pseudo_normed_group/LC.lean","src/pseudo_normed_group/profinitely_filtered.lean","src/pseudo_normed_group/system_of_complexes.lean","src/pseudo_normed_group/Tinv.lean","src/pseudo_normed_group/with_Tinv.lean","src/rescale/basic.lean","src/rescale/CLC.lean","src/rescale/FiltrationPow.lean","src/rescale/LC.lean","src/rescale/normed_group.lean","src/rescale/polyhedral_lattice.lean","src/rescale/pseudo_normed_group.lean","src/rescale/Tinv.lean","src/simplicial/alternating_face_map.lean","src/system_of_complexes/basic.lean","src/system_of_complexes/completion.lean","src/system_of_complexes/complex.lean","src/system_of_complexes/double.lean","src/system_of_complexes/rescale.lean","src/system_of_complexes/truncate.lean","src/thm95/constants.lean","src/thm95/default.lean","src/thm95/double_complex.lean","src/thm95/modify_complex.lean","src/thm95/polyhedral_iso.lean","src/thm95/row_iso.lean"]

the output i got tagging thm95 as the main declaration is at:
https://gist.github.com/alexjbest/57d5fead003dddd6931e8c0edcccc364

Alex J. Best (Apr 28 2021 at 23:18):

I don't know how sensible the output is tbh, there looks like a huge amount of stuff at present

Johan Commelin (Apr 29 2021 at 03:04):

Thanks. I'm actually not surprised that the list is long (-;

Johan Commelin (Apr 29 2021 at 03:05):

I'll sort the list, and then start working on the cleanup (-;

Johan Commelin (Apr 29 2021 at 03:16):

There are also lots of entries generated by @[simps]. Of course it would be cool if those can be filtered out. But I don't think it's too important.
The sorted output looks pretty useful to me. I'll report back how many of the 840 lines remain after a first go at cleaning up (-;

Johan Commelin (Apr 29 2021 at 03:43):

Oooh, one reason why the output is so long is because thm95/default.lean currently doesn't import and use the main result of thm95/row_iso.lean. But when I try to do that import, I get timeouts )-;

Johan Commelin (Apr 29 2021 at 03:44):

One reason I want to do the treeshaking now, is to make the entire project faster to compile again. Hopefully that will help in debugging what is wrong with that import between two of the high-level files in the project.

Johan Commelin (Apr 29 2021 at 04:25):

Wow, with

import tactic.find_unused
import thm95.default
import thm95.row_iso
#list_unused_decls ["src/breen_deligne/category.lean","src/breen_deligne/constants.lean","src/breen_deligne/eg.lean","src/breen_deligne/functorial_map.lean","src/breen_deligne/suitable.lean","src/breen_deligne/universal_map.lean","src/combinatorial_lemma.lean","src/facts/default.lean","src/facts/int.lean","src/facts/nnreal.lean","src/facts/normed_group.lean","src/for_mathlib/additive_functor.lean","src/for_mathlib/add_monoid_hom.lean","src/for_mathlib/arrow.lean","src/for_mathlib/big_operators_basic.lean","src/for_mathlib/category.lean","src/for_mathlib/curry.lean","src/for_mathlib/dfinsupp.lean","src/for_mathlib/equalizers.lean","src/for_mathlib/extend_from_nat.lean","src/for_mathlib/filter_at_top_bot.lean","src/for_mathlib/finsupp.lean","src/for_mathlib/Fintype/basic.lean","src/for_mathlib/free_abelian_group.lean","src/for_mathlib/Gordan.lean","src/for_mathlib/grading.lean","src/for_mathlib/grading_examples.lean","src/for_mathlib/grading_monoid_algebra.lean","src/for_mathlib/int_grading_lemma.lean","src/for_mathlib/kronecker.lean","src/for_mathlib/linear_algebra.lean","src/for_mathlib/nnreal.lean","src/for_mathlib/normed_group.lean","src/for_mathlib/normed_group_hom.lean","src/for_mathlib/normed_group_hom_bound_by.lean","src/for_mathlib/normed_group_hom_completion.lean","src/for_mathlib/normed_group_hom_equalizer.lean","src/for_mathlib/normed_group_quotient.lean","src/for_mathlib/order_basic.lean","src/for_mathlib/pi_nat_apply.lean","src/for_mathlib/preadditive_category.lean","src/for_mathlib/Profinite/basic.lean","src/for_mathlib/Profinite/functorial_limit.lean","src/for_mathlib/Profinite/limits.lean","src/for_mathlib/Profinite/locally_constant.lean","src/for_mathlib/Profinite/nhds.lean","src/for_mathlib/Profinite.lean","src/for_mathlib/pseudo_metric.lean","src/for_mathlib/quotient_group.lean","src/for_mathlib/real_Inf.lean","src/for_mathlib/simplicial/augmented.lean","src/for_mathlib/simplicial/complex.lean","src/for_mathlib/specific_limit.lean","src/for_mathlib/Top/limits.lean","src/for_mathlib/tsum.lean","src/for_mathlib/uniform_space_cauchy.lean","src/hacks_and_tricks/by_exactI_hack.lean","src/hacks_and_tricks/type_pow.lean","src/lem97.lean","src/liquid.lean","src/locally_constant/analysis.lean","src/locally_constant/NormedGroup.lean","src/locally_constant/Vhat.lean","src/Mbar/basic.lean","src/Mbar/bounded.lean","src/Mbar/Mbar_le.lean","src/Mbar/pseudo_normed_group.lean","src/normed_group/controlled_exactness.lean","src/normed_group/NormedGroup.lean","src/normed_group/normed_with_aut.lean","src/normed_group/pseudo_normed_group.lean","src/normed_snake.lean","src/normed_spectral.lean","src/partition.lean","src/polyhedral_lattice/basic.lean","src/polyhedral_lattice/category.lean","src/polyhedral_lattice/cech.lean","src/polyhedral_lattice/cosimplicial.lean","src/polyhedral_lattice/direct_sum.lean","src/polyhedral_lattice/finsupp.lean","src/polyhedral_lattice/Hom.lean","src/polyhedral_lattice/int.lean","src/polyhedral_lattice/pseudo_normed_group.lean","src/polyhedral_lattice/topology.lean","src/prop_92.lean","src/pseudo_normed_group/basic.lean","src/pseudo_normed_group/breen_deligne.lean","src/pseudo_normed_group/category.lean","src/pseudo_normed_group/CLC.lean","src/pseudo_normed_group/FiltrationPow.lean","src/pseudo_normed_group/homotopy.lean","src/pseudo_normed_group/LC.lean","src/pseudo_normed_group/profinitely_filtered.lean","src/pseudo_normed_group/system_of_complexes.lean","src/pseudo_normed_group/Tinv.lean","src/pseudo_normed_group/with_Tinv.lean","src/rescale/basic.lean","src/rescale/CLC.lean","src/rescale/FiltrationPow.lean","src/rescale/LC.lean","src/rescale/normed_group.lean","src/rescale/polyhedral_lattice.lean","src/rescale/pseudo_normed_group.lean","src/rescale/Tinv.lean","src/simplicial/alternating_face_map.lean","src/system_of_complexes/basic.lean","src/system_of_complexes/completion.lean","src/system_of_complexes/complex.lean","src/system_of_complexes/double.lean","src/system_of_complexes/rescale.lean","src/system_of_complexes/truncate.lean","src/thm95/constants.lean","src/thm95/default.lean","src/thm95/double_complex.lean","src/thm95/modify_complex.lean","src/thm95/polyhedral_iso.lean","src/thm95/row_iso.lean"]

at the top of my file (and thm95 and thm95.row_map_eq_sum_comp marked as main_declaration) I get ~1800 lines of output :shock:

Johan Commelin (Apr 29 2021 at 04:26):

Ooh, I used it wrong. I added the attribute in the files directly. But there they are unknown (-;

Johan Commelin (Apr 29 2021 at 04:27):

So this is what you need:

import tactic.find_unused

import breen_deligne.eg
import combinatorial_lemma
import thm95.row_iso
import liquid

attribute [main_declaration] thm95 thm95.row_map_eq_sum_comp first_target lem98
attribute [main_declaration] breen_deligne.eg.adept breen_deligne.eg.very_suitable

#list_unused_decls ["src/breen_deligne/category.lean","src/breen_deligne/constants.lean","src/breen_deligne/eg.lean","src/breen_deligne/functorial_map.lean","src/breen_deligne/suitable.lean","src/breen_deligne/universal_map.lean","src/combinatorial_lemma.lean","src/facts/default.lean","src/facts/int.lean","src/facts/nnreal.lean","src/facts/normed_group.lean","src/for_mathlib/additive_functor.lean","src/for_mathlib/add_monoid_hom.lean","src/for_mathlib/arrow.lean","src/for_mathlib/big_operators_basic.lean","src/for_mathlib/category.lean","src/for_mathlib/curry.lean","src/for_mathlib/dfinsupp.lean","src/for_mathlib/equalizers.lean","src/for_mathlib/extend_from_nat.lean","src/for_mathlib/filter_at_top_bot.lean","src/for_mathlib/finsupp.lean","src/for_mathlib/Fintype/basic.lean","src/for_mathlib/free_abelian_group.lean","src/for_mathlib/Gordan.lean","src/for_mathlib/grading.lean","src/for_mathlib/grading_examples.lean","src/for_mathlib/grading_monoid_algebra.lean","src/for_mathlib/int_grading_lemma.lean","src/for_mathlib/kronecker.lean","src/for_mathlib/linear_algebra.lean","src/for_mathlib/nnreal.lean","src/for_mathlib/normed_group.lean","src/for_mathlib/normed_group_hom.lean","src/for_mathlib/normed_group_hom_bound_by.lean","src/for_mathlib/normed_group_hom_completion.lean","src/for_mathlib/normed_group_hom_equalizer.lean","src/for_mathlib/normed_group_quotient.lean","src/for_mathlib/order_basic.lean","src/for_mathlib/pi_nat_apply.lean","src/for_mathlib/preadditive_category.lean","src/for_mathlib/Profinite/basic.lean","src/for_mathlib/Profinite/functorial_limit.lean","src/for_mathlib/Profinite/limits.lean","src/for_mathlib/Profinite/locally_constant.lean","src/for_mathlib/Profinite/nhds.lean","src/for_mathlib/Profinite.lean","src/for_mathlib/pseudo_metric.lean","src/for_mathlib/quotient_group.lean","src/for_mathlib/real_Inf.lean","src/for_mathlib/simplicial/augmented.lean","src/for_mathlib/simplicial/complex.lean","src/for_mathlib/specific_limit.lean","src/for_mathlib/Top/limits.lean","src/for_mathlib/tsum.lean","src/for_mathlib/uniform_space_cauchy.lean","src/hacks_and_tricks/by_exactI_hack.lean","src/hacks_and_tricks/type_pow.lean","src/lem97.lean","src/liquid.lean","src/locally_constant/analysis.lean","src/locally_constant/NormedGroup.lean","src/locally_constant/Vhat.lean","src/Mbar/basic.lean","src/Mbar/bounded.lean","src/Mbar/Mbar_le.lean","src/Mbar/pseudo_normed_group.lean","src/normed_group/controlled_exactness.lean","src/normed_group/NormedGroup.lean","src/normed_group/normed_with_aut.lean","src/normed_group/pseudo_normed_group.lean","src/normed_snake.lean","src/normed_spectral.lean","src/partition.lean","src/polyhedral_lattice/basic.lean","src/polyhedral_lattice/category.lean","src/polyhedral_lattice/cech.lean","src/polyhedral_lattice/cosimplicial.lean","src/polyhedral_lattice/direct_sum.lean","src/polyhedral_lattice/finsupp.lean","src/polyhedral_lattice/Hom.lean","src/polyhedral_lattice/int.lean","src/polyhedral_lattice/pseudo_normed_group.lean","src/polyhedral_lattice/topology.lean","src/prop_92.lean","src/pseudo_normed_group/basic.lean","src/pseudo_normed_group/breen_deligne.lean","src/pseudo_normed_group/category.lean","src/pseudo_normed_group/CLC.lean","src/pseudo_normed_group/FiltrationPow.lean","src/pseudo_normed_group/homotopy.lean","src/pseudo_normed_group/LC.lean","src/pseudo_normed_group/profinitely_filtered.lean","src/pseudo_normed_group/system_of_complexes.lean","src/pseudo_normed_group/Tinv.lean","src/pseudo_normed_group/with_Tinv.lean","src/rescale/basic.lean","src/rescale/CLC.lean","src/rescale/FiltrationPow.lean","src/rescale/LC.lean","src/rescale/normed_group.lean","src/rescale/polyhedral_lattice.lean","src/rescale/pseudo_normed_group.lean","src/rescale/Tinv.lean","src/simplicial/alternating_face_map.lean","src/system_of_complexes/basic.lean","src/system_of_complexes/completion.lean","src/system_of_complexes/complex.lean","src/system_of_complexes/double.lean","src/system_of_complexes/rescale.lean","src/system_of_complexes/truncate.lean","src/thm95/constants.lean","src/thm95/default.lean","src/thm95/double_complex.lean","src/thm95/modify_complex.lean","src/thm95/polyhedral_iso.lean","src/thm95/row_iso.lean"]

Johan Commelin (Apr 29 2021 at 04:47):

And then

cat unused-liquid-presort.lean | cut -f2 -d' ' > unused-liquid-col2
git grep -ohf unused-liquid-col2.lean | sort | uniq > unused-liquid.sorted

which gives a file with ~150 lines

Johan Commelin (Apr 29 2021 at 04:50):

Hmm, that's of course dangerous, because some of the lines might not have matched due to open namespaces...

Johan Commelin (Apr 29 2021 at 04:50):

So it's not a very good way of filtering out the auto-generated stuff

Johan Commelin (Apr 29 2021 at 05:14):

I think it would be really useful if Lean could also filter this list so that it only prints defs

Johan Commelin (Apr 29 2021 at 05:14):

@Alex J. Best do you know if you can check whether a decl is def or lemma via metaprogramming?

Johan Commelin (Apr 29 2021 at 05:16):

That would also get rid of all the autogenerated stuff, because I don't think there are autogenerated defs.

Alex J. Best (Apr 29 2021 at 05:17):

Yes you can check with docs#declaration.is_definition or docs#declaration.is_theorem (this matches lemmas too)

Alex J. Best (Apr 29 2021 at 05:19):

There is also docs#declaration.is_auto_generated and docs#declaration.is_auto_or_internal which may be useful?

Johan Commelin (Apr 29 2021 at 05:21):

aah, thanks...

Johan Commelin (Apr 29 2021 at 05:21):

Is there a way to get a list out of unused_decls? instead of manually copy-pasting the output message with all the #print bla?

Johan Commelin (Apr 29 2021 at 05:22):

Aside: it looks like we never use the category ProFiltPseuNormGrp, only ProFiltPseuNormGrpWithTinv. This list is pretty useful.

Johan Commelin (Apr 29 2021 at 05:22):

I've already removed > 600 lines from the project.

Johan Commelin (Apr 29 2021 at 05:24):

I just pushed

Alex J. Best (Apr 29 2021 at 05:35):

does something like this do what you want?

import tactic.find_unused

open tactic

run_cmd (
do ds ← all_unused [none, "src/breen_deligne/category.lean","src/breen_deligne/constants.lean","src/breen_deligne/eg.lean","src/breen_deligne/functorial_map.lean","src/breen_deligne/suitable.lean","src/breen_deligne/universal_map.lean","src/combinatorial_lemma.lean","src/facts/default.lean","src/facts/int.lean","src/facts/nnreal.lean","src/facts/normed_group.lean","src/for_mathlib/additive_functor.lean","src/for_mathlib/add_monoid_hom.lean","src/for_mathlib/arrow.lean","src/for_mathlib/big_operators_basic.lean","src/for_mathlib/category.lean","src/for_mathlib/curry.lean","src/for_mathlib/dfinsupp.lean","src/for_mathlib/equalizers.lean","src/for_mathlib/extend_from_nat.lean","src/for_mathlib/filter_at_top_bot.lean","src/for_mathlib/finsupp.lean","src/for_mathlib/Fintype/basic.lean","src/for_mathlib/free_abelian_group.lean","src/for_mathlib/Gordan.lean","src/for_mathlib/grading.lean","src/for_mathlib/grading_examples.lean","src/for_mathlib/grading_monoid_algebra.lean","src/for_mathlib/int_grading_lemma.lean","src/for_mathlib/kronecker.lean","src/for_mathlib/linear_algebra.lean","src/for_mathlib/nnreal.lean","src/for_mathlib/normed_group.lean","src/for_mathlib/normed_group_hom.lean","src/for_mathlib/normed_group_hom_bound_by.lean","src/for_mathlib/normed_group_hom_completion.lean","src/for_mathlib/normed_group_hom_equalizer.lean","src/for_mathlib/normed_group_quotient.lean","src/for_mathlib/order_basic.lean","src/for_mathlib/pi_nat_apply.lean","src/for_mathlib/preadditive_category.lean","src/for_mathlib/Profinite/basic.lean","src/for_mathlib/Profinite/functorial_limit.lean","src/for_mathlib/Profinite/limits.lean","src/for_mathlib/Profinite/locally_constant.lean","src/for_mathlib/Profinite/nhds.lean","src/for_mathlib/Profinite.lean","src/for_mathlib/pseudo_metric.lean","src/for_mathlib/quotient_group.lean","src/for_mathlib/real_Inf.lean","src/for_mathlib/simplicial/augmented.lean","src/for_mathlib/simplicial/complex.lean","src/for_mathlib/specific_limit.lean","src/for_mathlib/Top/limits.lean","src/for_mathlib/tsum.lean","src/for_mathlib/uniform_space_cauchy.lean","src/hacks_and_tricks/by_exactI_hack.lean","src/hacks_and_tricks/type_pow.lean","src/lem97.lean","src/liquid.lean","src/locally_constant/analysis.lean","src/locally_constant/NormedGroup.lean","src/locally_constant/Vhat.lean","src/Mbar/basic.lean","src/Mbar/bounded.lean","src/Mbar/Mbar_le.lean","src/Mbar/pseudo_normed_group.lean","src/normed_group/controlled_exactness.lean","src/normed_group/NormedGroup.lean","src/normed_group/normed_with_aut.lean","src/normed_group/pseudo_normed_group.lean","src/normed_snake.lean","src/normed_spectral.lean","src/partition.lean","src/polyhedral_lattice/basic.lean","src/polyhedral_lattice/category.lean","src/polyhedral_lattice/cech.lean","src/polyhedral_lattice/cosimplicial.lean","src/polyhedral_lattice/direct_sum.lean","src/polyhedral_lattice/finsupp.lean","src/polyhedral_lattice/Hom.lean","src/polyhedral_lattice/int.lean","src/polyhedral_lattice/pseudo_normed_group.lean","src/polyhedral_lattice/topology.lean","src/prop_92.lean","src/pseudo_normed_group/basic.lean","src/pseudo_normed_group/breen_deligne.lean","src/pseudo_normed_group/category.lean","src/pseudo_normed_group/CLC.lean","src/pseudo_normed_group/FiltrationPow.lean","src/pseudo_normed_group/homotopy.lean","src/pseudo_normed_group/LC.lean","src/pseudo_normed_group/profinitely_filtered.lean","src/pseudo_normed_group/system_of_complexes.lean","src/pseudo_normed_group/Tinv.lean","src/pseudo_normed_group/with_Tinv.lean","src/rescale/basic.lean","src/rescale/CLC.lean","src/rescale/FiltrationPow.lean","src/rescale/LC.lean","src/rescale/normed_group.lean","src/rescale/polyhedral_lattice.lean","src/rescale/pseudo_normed_group.lean","src/rescale/Tinv.lean","src/simplicial/alternating_face_map.lean","src/system_of_complexes/basic.lean","src/system_of_complexes/completion.lean","src/system_of_complexes/complex.lean","src/system_of_complexes/double.lean","src/system_of_complexes/rescale.lean","src/system_of_complexes/truncate.lean","src/thm95/constants.lean","src/thm95/default.lean","src/thm95/double_complex.lean","src/thm95/modify_complex.lean","src/thm95/polyhedral_iso.lean","src/thm95/row_iso.lean"],
let ds := ds.filter (λ t, declaration.is_theorem t),
tactic.trace (ds.to_list.map $ λ ⟨n,_⟩, n))

Alex J. Best (Apr 29 2021 at 05:35):

docs#all_unused already filters by is_auto_or_internal it seems

Johan Commelin (Apr 29 2021 at 06:12):

@Alex J. Best Let me try it out! Are simp-lemmas generated by @[simps] tagged as is_auto?

Alex J. Best (Apr 29 2021 at 06:15):

I don't think they are, I believe auto-generated in this context just means the rec_on and no_confusion sort of auto-generated things. Not things added by mathlib tactics like simps.

Johan Commelin (Apr 29 2021 at 06:17):

Hmm, you were filtering for theorems, I changed that to defs. The result looks useful.

Johan Commelin (Apr 29 2021 at 06:21):

@Alex J. Best can you make the trace output print one decl per line, without the [.., ..] list brackets and commas?

Johan Commelin (Apr 29 2021 at 06:25):

My attempt:

meta def file_list : list (option string) :=
["src/breen_deligne/category.lean","src/breen_deligne/constants.lean","src/breen_deligne/eg.lean","src/breen_deligne/functorial_map.lean","src/breen_deligne/suitable.lean","src/breen_deligne/universal_map.lean","src/combinatorial_lemma.lean","src/facts/default.lean","src/facts/int.lean","src/facts/nnreal.lean","src/facts/normed_group.lean","src/for_mathlib/additive_functor.lean","src/for_mathlib/add_monoid_hom.lean","src/for_mathlib/arrow.lean","src/for_mathlib/big_operators_basic.lean","src/for_mathlib/category.lean","src/for_mathlib/curry.lean","src/for_mathlib/dfinsupp.lean","src/for_mathlib/equalizers.lean","src/for_mathlib/extend_from_nat.lean","src/for_mathlib/filter_at_top_bot.lean","src/for_mathlib/finsupp.lean","src/for_mathlib/Fintype/basic.lean","src/for_mathlib/free_abelian_group.lean","src/for_mathlib/Gordan.lean","src/for_mathlib/grading.lean","src/for_mathlib/grading_examples.lean","src/for_mathlib/grading_monoid_algebra.lean","src/for_mathlib/int_grading_lemma.lean","src/for_mathlib/kronecker.lean","src/for_mathlib/linear_algebra.lean","src/for_mathlib/nnreal.lean","src/for_mathlib/normed_group.lean","src/for_mathlib/normed_group_hom.lean","src/for_mathlib/normed_group_hom_bound_by.lean","src/for_mathlib/normed_group_hom_completion.lean","src/for_mathlib/normed_group_hom_equalizer.lean","src/for_mathlib/normed_group_quotient.lean","src/for_mathlib/order_basic.lean","src/for_mathlib/pi_nat_apply.lean","src/for_mathlib/preadditive_category.lean","src/for_mathlib/Profinite/basic.lean","src/for_mathlib/Profinite/functorial_limit.lean","src/for_mathlib/Profinite/limits.lean","src/for_mathlib/Profinite/locally_constant.lean","src/for_mathlib/Profinite/nhds.lean","src/for_mathlib/Profinite.lean","src/for_mathlib/pseudo_metric.lean","src/for_mathlib/quotient_group.lean","src/for_mathlib/real_Inf.lean","src/for_mathlib/simplicial/augmented.lean","src/for_mathlib/simplicial/complex.lean","src/for_mathlib/specific_limit.lean","src/for_mathlib/Top/limits.lean","src/for_mathlib/tsum.lean","src/for_mathlib/uniform_space_cauchy.lean","src/hacks_and_tricks/by_exactI_hack.lean","src/hacks_and_tricks/type_pow.lean","src/lem97.lean","src/liquid.lean","src/locally_constant/analysis.lean","src/locally_constant/NormedGroup.lean","src/locally_constant/Vhat.lean","src/Mbar/basic.lean","src/Mbar/bounded.lean","src/Mbar/Mbar_le.lean","src/Mbar/pseudo_normed_group.lean","src/normed_group/controlled_exactness.lean","src/normed_group/NormedGroup.lean","src/normed_group/normed_with_aut.lean","src/normed_group/pseudo_normed_group.lean","src/normed_snake.lean","src/normed_spectral.lean","src/partition.lean","src/polyhedral_lattice/basic.lean","src/polyhedral_lattice/category.lean","src/polyhedral_lattice/cech.lean","src/polyhedral_lattice/cosimplicial.lean","src/polyhedral_lattice/direct_sum.lean","src/polyhedral_lattice/finsupp.lean","src/polyhedral_lattice/Hom.lean","src/polyhedral_lattice/int.lean","src/polyhedral_lattice/pseudo_normed_group.lean","src/polyhedral_lattice/topology.lean","src/prop_92.lean","src/pseudo_normed_group/basic.lean","src/pseudo_normed_group/breen_deligne.lean","src/pseudo_normed_group/category.lean","src/pseudo_normed_group/CLC.lean","src/pseudo_normed_group/FiltrationPow.lean","src/pseudo_normed_group/homotopy.lean","src/pseudo_normed_group/LC.lean","src/pseudo_normed_group/profinitely_filtered.lean","src/pseudo_normed_group/system_of_complexes.lean","src/pseudo_normed_group/Tinv.lean","src/pseudo_normed_group/with_Tinv.lean","src/rescale/basic.lean","src/rescale/CLC.lean","src/rescale/FiltrationPow.lean","src/rescale/LC.lean","src/rescale/normed_group.lean","src/rescale/polyhedral_lattice.lean","src/rescale/pseudo_normed_group.lean","src/rescale/Tinv.lean","src/simplicial/alternating_face_map.lean","src/system_of_complexes/basic.lean","src/system_of_complexes/completion.lean","src/system_of_complexes/complex.lean","src/system_of_complexes/double.lean","src/system_of_complexes/rescale.lean","src/system_of_complexes/truncate.lean","src/thm95/constants.lean","src/thm95/default.lean","src/thm95/double_complex.lean","src/thm95/modify_complex.lean","src/thm95/polyhedral_iso.lean","src/thm95/row_iso.lean"]

open tactic

meta def unused_defs (fs : list (option string)) : tactic unit :=
do ds ← all_unused fs,
let ds := ds.filter (λ t, declaration.is_definition t),
let ds' := (ds.to_list.map $ λ ⟨n,_⟩, n.to_string),
let ds'' := string.intercalate "\n" ds',
tactic.trace ds''

run_cmd unused_defs file_list

Johan Commelin (Apr 29 2021 at 06:27):

Seems to work. 172 definitions aren't being used :rofl:

Alex J. Best (Apr 29 2021 at 07:05):

Johan Commelin said:

Hmm, you were filtering for theorems, I changed that to defs. The result looks useful.

Oops I misread what you wrote earlier yes.
And yes that looks good to me! I guess the reason none was in the original file list was that none represented the current file, but seeing as the list includes thm95/default.lean anyway it was actually duplicated.

Johan Commelin (Apr 29 2021 at 07:33):

:tada: I found the timeout issue between row_iso.lean and default.lean

Johan Commelin (Apr 29 2021 at 07:34):

I had to mark some things as irreducible because I made them reducible but forgot the local prefix.

Kevin Buzzard (Apr 29 2021 at 11:55):

Oh that's great news!

Johan Commelin (Jul 18 2022 at 13:53):

Just bumping this thread to remind me that we should try to do some treeshaking again.

Johan Commelin (Jul 20 2022 at 06:47):

I'm running the treeshake on the mathlib bump thread atm.

Johan Commelin (Jul 20 2022 at 06:59):

Here's the output https://gist.github.com/jcommelin/90b42c047ec1959abe8a359ae5fd0d57

Johan Commelin (Jul 20 2022 at 06:59):

Note that this only lists unused definitions!

Johan Commelin (Jul 20 2022 at 07:01):

Some surprising entries!

ExtrDisc.topological_space

Johan Commelin (Jul 20 2022 at 07:06):

Here is the Lean file I used: based on @Alex J. Best's code upstairs
https://gist.github.com/jcommelin/54a31030dba0511cb2efaf66082f7694

Johan Commelin (Jul 20 2022 at 07:26):

Another surprise:

thm95.universal_constants.K₀

Looks like we are making life more complicated than necessary, when computing those constants.

Alex J. Best (Jul 20 2022 at 09:08):

Here is a way to get the file list automatically, by asking lean to call find rather than copypasta

import tactic
.

open tactic
def tree_args (src : string) : io.process.spawn_args :=
{ cmd := "find",
  args := src :: ["-type", "f", "-name", "*.lean", "-print"], }

run_cmd do
  s ← unsafe_run_io $ io.cmd $ tree_args "src",
  let fs := s.split_on '\n',
  trace fs

Johan Commelin (Jul 20 2022 at 09:52):

Nice! That's a lot cleaner.

Eric Wieser (Jul 20 2022 at 10:46):

Can you emit file and line numbers too so that you can link to github for each def?

Johan Commelin (Jul 20 2022 at 10:54):

@Eric Wieser Do you know how to grab that info using meta-programming?

Eric Wieser (Jul 20 2022 at 10:54):

Yes, I do it here: https://github.com/eric-wieser/lean-graded-rings/blob/9812eb5ec02962fa1e3ce22a9418eb9439b8d2b7/export.lean#L25

Eric Wieser (Jul 20 2022 at 10:55):

docs#environment.decl_pos and docs#environment.decl_olean

Johan Commelin (Jul 20 2022 at 11:05):

Once the mathlib bump is merged, I'll add scripts/treeshake.lean using both suggestions.

Last updated: Dec 20 2023 at 11:08 UTC

Stream: condensed mathematics

Topic: treeshaking

Johan Commelin (Apr 28 2021 at 06:38):

Alex J. Best (Apr 28 2021 at 23:13):

Alex J. Best (Apr 28 2021 at 23:18):

Johan Commelin (Apr 29 2021 at 03:04):

Johan Commelin (Apr 29 2021 at 03:05):

Johan Commelin (Apr 29 2021 at 03:16):

Johan Commelin (Apr 29 2021 at 03:43):

Johan Commelin (Apr 29 2021 at 03:44):

Johan Commelin (Apr 29 2021 at 04:25):

Johan Commelin (Apr 29 2021 at 04:26):

Johan Commelin (Apr 29 2021 at 04:27):

Johan Commelin (Apr 29 2021 at 04:47):

Johan Commelin (Apr 29 2021 at 04:50):

Johan Commelin (Apr 29 2021 at 04:50):

Johan Commelin (Apr 29 2021 at 05:14):

Johan Commelin (Apr 29 2021 at 05:14):

Johan Commelin (Apr 29 2021 at 05:16):

Alex J. Best (Apr 29 2021 at 05:17):

Alex J. Best (Apr 29 2021 at 05:19):

Johan Commelin (Apr 29 2021 at 05:21):

Johan Commelin (Apr 29 2021 at 05:21):

Johan Commelin (Apr 29 2021 at 05:22):

Johan Commelin (Apr 29 2021 at 05:22):

Johan Commelin (Apr 29 2021 at 05:24):

Alex J. Best (Apr 29 2021 at 05:35):

Alex J. Best (Apr 29 2021 at 05:35):

Johan Commelin (Apr 29 2021 at 06:12):

Alex J. Best (Apr 29 2021 at 06:15):

Johan Commelin (Apr 29 2021 at 06:17):

Johan Commelin (Apr 29 2021 at 06:21):

Johan Commelin (Apr 29 2021 at 06:25):

Johan Commelin (Apr 29 2021 at 06:27):

Alex J. Best (Apr 29 2021 at 07:05):

Johan Commelin (Apr 29 2021 at 07:33):

Johan Commelin (Apr 29 2021 at 07:34):

Kevin Buzzard (Apr 29 2021 at 11:55):

Johan Commelin (Jul 18 2022 at 13:53):

Johan Commelin (Jul 20 2022 at 06:47):

Johan Commelin (Jul 20 2022 at 06:59):

Johan Commelin (Jul 20 2022 at 06:59):

Johan Commelin (Jul 20 2022 at 07:01):

Johan Commelin (Jul 20 2022 at 07:06):

Johan Commelin (Jul 20 2022 at 07:26):

Alex J. Best (Jul 20 2022 at 09:08):

Johan Commelin (Jul 20 2022 at 09:52):

Eric Wieser (Jul 20 2022 at 10:46):

Johan Commelin (Jul 20 2022 at 10:54):

Eric Wieser (Jul 20 2022 at 10:54):

Eric Wieser (Jul 20 2022 at 10:55):

Johan Commelin (Jul 20 2022 at 11:05):