cache regenerating

Stream: general

[Kevin Buzzard]

buzzard@ebony:~/lean-projects/lean-perfectoid-spaces$ lean --make
/home/buzzard/lean-projects/lean-perfectoid-spaces/_target/deps/mathlib/src/group_theory/quotient_group.lean: parsing at line 42cache regenerating
/home/buzzard/lean-projects/lean-perfectoid-spaces/_target/deps/mathlib/test/local_cache.lean: parsing at line 67cache regenerating
/home/buzzard/lean-projects/lean-perfectoid-spaces/_target/deps/mathlib/src/tactic/linarith.lean: linarith.int.coe_nat_bit0_mulcache regenerating
/home/buzzard/lean-projects/lean-perfectoid-spaces/_target/deps/mathlib/src/tactic/linarith.lean: linarith.int.coe_nat_zero_mulcache regenerating
/home/buzzard/lean-projects/lean-perfectoid-spaces/_target/deps/mathlib/src/tactic/linarith.lean: linarith.nat_eq_substcache regenerating
/home/buzzard/lean-projects/lean-perfectoid-spaces/_target/deps/mathlib/src/tactic/linarith.lean: linarith.nat_lt_substcache regenerating
/home/buzzard/lean-projects/lean-perfectoid-spaces/_target/deps/mathlib/src/tactic/linarith.lean: parsing at line 49cache regenerating
/home/buzzard/lean-projects/lean-perfectoid-spaces/_target/deps/mathlib/src/group_theory/quotient_group.lean: parsing at line 69cache regenerating
/home/buzzard/lean-projects/lean-perfectoid-spaces/_target/deps/mathlib/src/tactic/linarith.lean: linarith.le_of_le_of_eqcache regenerating
/home/buzzard/lean-projects/lean-perfectoid-spaces/_target/deps/mathlib/src/tactic/linarith.lean: linarith.mul_eqcache regenerating
/home/buzzard/lean-projects/lean-perfectoid-spaces/_target/deps/mathlib/src/tactic/ring2.lean: tactic.ring2.horner_expr.cseval_add_constcache regenerating
/home/buzzard/lean-projects/lean-perfectoid-spaces/_target/deps/mathlib/test/local_cache.lean: parsing at line 285cache regenerating
/home/buzzard/lean-projects/lean-perfectoid-spaces/_target/deps/mathlib/test/local_cache.lean: parsing at line 306cache regenerating
/home/buzzard/lean-projects/lean-perfectoid-spaces/_target/deps/mathlib/src/tactic/ring2.lean: parsing at line 446cache regenerating
/home/buzzard/lean-projects/lean-perfectoid-spaces/_target/deps/mathlib/src/data/padics/padic_norm.lean: parsing at line 307cache regenerating
/home/buzzard/lean-projects/lean-perfectoid-spaces/_target/deps/mathlib/src/group_theory/perm/cycles.lean: parsing at line 1cache regenerating
cache regenerating
/home/buzzard/lean-projects/lean-perfectoid-spaces/_target/deps/mathlib/src/group_theory/quotient_group.lean: parsing at line 123cache regenerating
/home/buzzard/lean-projects/lean-perfectoid-spaces/_target/deps/mathlib/test/local_cache.lean: def_local.my_lemma_2cache regenerating
/home/buzzard/lean-projects/lean-perfectoid-spaces/_target/deps/mathlib/src/algebra/module.lean: parsing at line 45cache regenerating
/home/buzzard/lean-projects/lean-perfectoid-spaces/_target/deps/mathlib/src/algebra/module.lean: parsing at line 58cache regenerating
/home/buzzard/lean-projects/lean-perfectoid-spaces/_target/deps/mathlib/src/computability/partrec.lean: nat.partrec.of_primreccache regenerating
cache regenerating
cache regenerating
/home/buzzard/lean-projects/lean-perfectoid-spaces/_target/deps/mathlib/src/tactic/linarith.lean: parsing at line 276cache regenerating
cache regenerating

This is all very exciting. Is my cache supposed to be regenerating?

[Kevin Buzzard]

Am I just compiling too much? I usually only compile src

[Keeley Hoek]

Hey Kevin, this one's on me; thats a whole bunch of tests in test/local_cache.lean being run as I understand it

[Keeley Hoek]

All of the other tests are silent I believe

[Kevin Buzzard]

Aah I see, so it's just that I accidentally compiled the stuff in test which I usually leave alone.

[Keeley Hoek]

I think so!

[Simon Hudon]

I think we should make that test quiet as well