unknown declaration `_private`

Stream: CI

[Riccardo Brasca]

#11396 fails on continuous integration / Run tests (push) with

<unknown>:1:1: error: unknown declaration '_private.3777865389.ne_from_not_eq'
Error: Process completed with exit code 1.

[Anne Baanen]

It reads as though a private definition should become public somehow. Or maybe this is a hash collision?

[Anne Baanen]

Seems to be the same as this thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/error.3A.20unknown.20declaration.20_private

[Riccardo Brasca]

ne_from_not_eq esists as a private declaration (it is in src/tactic/norm_cast.lean), but it seems unrelated to my PR...

[Eric Rodriguez]

this seems to be an error that pops up randomly. if you make any nonsense change in your commit, it should go away next push

[Riccardo Brasca]

Let me try

[Riccardo Brasca]

Mmm, I keep on getting the same error. I am trying to make the declaration public to see what happens.

[Anne Baanen]

I just got the same error :cry:

[Eric Rodriguez]

argh, what is going on... is it worth making detect_errors temporarily dump the full commandline output to figure out what it is? i'm gonna try build one of these locally to see if I can get the error

[Alex J. Best]

I've been trying this for the past 10 mins or so

[Alex J. Best]

I can reproduce the error locally, but still not really any closer to diagnosing it

[Eric Rodriguez]

argh, yeah, the output isn't helpful diagnosing wise:

 ~/r/mathlib  on reverse-submodule_norm_coe  lean --json -T100000 --make docs archive roadmap test counterexamples

{"caption":"","file_name":"/Users/ericr/repos/mathlib/counterexamples/phillips.lean","pos_col":4,"pos_line":110,"severity":"error","text":"unknown declaration '_private.579854401.pseudo_metric_space.dist_nonneg''"}
{"caption":"","file_name":"/Users/ericr/repos/mathlib/counterexamples/phillips.lean","pos_col":8,"pos_line":134,"severity":"error","text":"type mismatch at application\n  Exists.intro φ (λ (f : discrete_copy α →ᵇ ℝ) (hf : integrable ⇑f μ), hφ.left ⟨f, hf⟩)\nterm\n  λ (f : discrete_copy α →ᵇ ℝ) (hf : integrable ⇑f μ), hφ.left ⟨f, hf⟩\nhas type\n  ∀ (f : discrete_copy α →ᵇ ℝ) (hf : integrable ⇑f μ),\n    ⇑φ ↑⟨f, hf⟩ = ⇑(bounded_integrable_functions_integral_clm μ) ⟨f, hf⟩\nbut is expected to have type\n  ∀ (f : discrete_copy α →ᵇ ℝ), integrable ⇑f μ → ⇑φ f = ∫ (x : α), ⇑f x ∂μ\nstate:\nα : Type u,\n_inst_1 : measurable_space α,\nμ : measure α,\n_inst_2 : is_finite_measure μ,\nφ : (discrete_copy α →ᵇ ℝ) →L[ℝ] ℝ,\nhφ :\n  (∀ (x : ↥(bounded_integrable_functions μ)), ⇑φ ↑x = ⇑(bounded_integrable_functions_integral_clm μ) x) ∧\n    ∥φ∥ = ∥bounded_integrable_functions_integral_clm μ∥\n⊢ ∃ (φ : (discrete_copy α →ᵇ ℝ) →L[ℝ] ℝ),\n    ∀ (f : discrete_copy α →ᵇ ℝ), integrable ⇑f μ → ⇑φ f = ∫ (x : α), ⇑f x ∂μ"}
{"caption":"","file_name":"/Users/ericr/repos/mathlib/counterexamples/phillips.lean","pos_col":0,"pos_line":569,"severity":"error","text":"unknown declaration '_private.579854401.pseudo_metric_space.dist_nonneg''"}

[Gabriel Ebner]

Or maybe this is a hash collision?

Can you try adding a space to src/tactic/doc_commands.lean and see if this make CI happy?

[Rob Lewis]

This has been coming up rarely but periodically. I saw it the other day but didn't have time to diagnose

[Rob Lewis]

Merging master usually fixes it but a real diagnosis would be great!

[Alex J. Best]

I'm not sure if it's a diagnosis, more a sequence of observations but when I get riccardo's PR ea4acc9aba6d6d7033675705809a28b4acbc796a and get the mathlib cache the following fails lean --recursive --export=mathlib2.txt src/algebra/char_zero.lean --only-export=nat.cast_add_one_ne_zero with error <unknown>:1:1: error: unknown declaration '_private.3777865389.ne_from_not_eq'.
This is in the term of docs#nat.cast_add_one_ne_zero because that uses exact_mod_cast which uses its own private lemmas in its proofs.
The interesting thing is that many other oleans have ne_from_not_eq in, grep gives me

Binary file .//src/tactic/norm_cast.olean matches
Binary file .//src/topology/metric_space/contracting.olean matches
Binary file .//src/analysis/complex/roots_of_unity.olean matches
Binary file .//src/analysis/special_functions/trigonometric/arctan.olean matches
Binary file .//src/analysis/special_functions/trigonometric/arctan_deriv.olean matches
Binary file .//src/analysis/special_functions/integrals.olean matches
Binary file .//src/analysis/special_functions/pow.olean matches
Binary file .//src/analysis/normed/group/quotient.olean matches
Binary file .//src/analysis/fourier.olean matches
Binary file .//src/number_theory/liouville/liouville_with.olean matches
Binary file .//src/number_theory/padics/ring_homs.olean matches
Binary file .//src/number_theory/padics/padic_norm.olean matches
Binary file .//src/number_theory/padics/padic_numbers.olean matches
Binary file .//src/number_theory/padics/padic_integers.olean matches
Binary file .//src/number_theory/bernoulli.olean matches
Binary file .//src/number_theory/modular.olean matches
Binary file .//src/number_theory/bernoulli_polynomials.olean matches
Binary file .//src/number_theory/pythagorean_triples.olean matches
Binary file .//src/number_theory/class_number/finite.olean matches
Binary file .//src/measure_theory/measure/hausdorff.olean matches
Binary file .//src/group_theory/free_abelian_group_finsupp.olean matches
Binary file .//src/group_theory/specific_groups/cyclic.olean matches
Binary file .//src/ring_theory/witt_vector/witt_polynomial.olean matches
Binary file .//src/ring_theory/witt_vector/frobenius.olean matches
Binary file .//src/ring_theory/witt_vector/structure_polynomial.olean matches
Binary file .//src/geometry/euclidean/monge_point.olean matches
Binary file .//src/data/complex/exponential.olean matches
Binary file .//src/data/real/ennreal.olean matches
Binary file .//src/data/real/pi/wallis.olean matches
Binary file .//src/data/real/pi/leibniz.olean matches
Binary file .//src/data/real/nnreal.olean matches
Binary file .//src/data/real/irrational.olean matches
Binary file .//src/data/nat/modeq.olean matches
Binary file .//src/data/rat/floor.olean matches
Binary file .//src/data/rat/basic.olean matches
Binary file .//src/data/polynomial/hasse_deriv.olean matches
Binary file .//src/algebra/char_p/invertible.olean matches
Binary file .//src/algebra/char_zero.olean matches

picking one of these other files like contracting.olean and opening it in hexedit I see

5F 70 72 69  76 61 74 65  00 FF B5 BD  BB 25 6E 65  5F 66 72 6F  6D 5F 6E 6F  74 5F 65 71

this is _private.3049110309.ne_from_not_eq. (I'm sure there is an easier way to do this than hexedit lol but olean-rs wasn't working for me). This indeed references a somewhat consistent name as it is the same as in the output of lean --recursive --export=mathlib4.txt src/data/nat/cast.lean, and all of these oleans I checked use 3049110309 not 3777865389.
If I manually replace that tiny portion of src/algebra/char_zero.olean with _private.3049110309.ne_from_not_eq instead of _private.3777865389.ne_from_not_eq (B5 BD BB 25 with E1 2D A6 AD) then everything looks like it builds fine, at least lean --recursive --export=mathlib5.txt src/algebra/char_zero.lean then works.

The question seems to be why does one olean think the private name is one thing, while all the others think its different

[Riccardo Brasca]

I confirm that merging master fixed the problem.