Zulip Chat Archive

Stream: general

Topic: cache regenerating


Kevin Buzzard (Apr 15 2019 at 10:38):

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 (Apr 15 2019 at 10:39):

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

Keeley Hoek (Apr 15 2019 at 11:00):

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 (Apr 15 2019 at 11:00):

All of the other tests are silent I believe

Kevin Buzzard (Apr 15 2019 at 11:04):

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

Keeley Hoek (Apr 15 2019 at 11:05):

I think so!

Simon Hudon (Apr 15 2019 at 13:48):

I think we should make that test quiet as well


Last updated: Dec 20 2023 at 11:08 UTC