Strange CI errors

Stream: new members

[Snir Broshi]

I'm seeing strange errors in the latest CI builds of #30263 and I'm not sure if it's something I can fix:

First run: verify that everything was available in the cache failed on the file the PR modifies:

  ✖ [741/931] Building Mathlib.Algebra.Order.Ring.Unbundled.Rat
  error: target is out-of-date and needs to be rebuilt

Then I tried merging master to maybe get updates for CI scripts, and the second run is weirder:

✖ [4038/7386] Building Mathlib.Tactic.NormNum.Inv (1.8s)
Error: error: Mathlib/Tactic/NormNum/Inv.lean:69:2: (interpreter) unknown declaration 'Mathlib.Meta.NormNum.evalMkRat'
Error: error: Mathlib/Tactic/NormNum/Inv.lean:70:4: Unknown constant `Lean.throwError._at_.Lean.throwErrorAt._at_.Lean.throwUnknownIdentifierAt._at_.Lean.throwUnknownConstantAt._at_.Lean.throwUnknownConstant._at_.Lean.getConstInfo._at_.Lean.getConstInfoCtor._at_._private.Plausible.DeriveArbitrary.0.Plausible.getCtorArgsNamesAndTypes.spec_1.spec_1.spec_1.spec_1.spec_1.spec_3.spec_3`
Error: error: Mathlib/Tactic/NormNum/Inv.lean:158:4: Unknown constant `Lean.throwError._at_.Lean.throwErrorAt._at_.Lean.throwUnknownIdentifierAt._at_.Lean.throwUnknownConstantAt._at_.Lean.throwUnknownConstant._at_.Lean.getConstInfo._at_.Lean.getConstInfoCtor._at_._private.Plausible.DeriveArbitrary.0.Plausible.getCtorArgsNamesAndTypes.spec_1.spec_1.spec_1.spec_1.spec_1.spec_3.spec_3`
Error: error: Mathlib/Tactic/NormNum/Inv.lean:200:2: (interpreter) unknown declaration 'Mathlib.Meta.NormNum.evalInv'
Error: error: Mathlib/Tactic/NormNum/Inv.lean:200:20: failed to compile definition, compiler IR check failed at `Mathlib.Meta.NormNum.evalInv._lam_1`. Error: depends on declaration 'Mathlib.Meta.NormNum.Result.inv', which has no executable code; consider marking definition as 'noncomputable'
error: Lean exited with code 1
✖ [6932/7386] Building Mathlib.Tactic.Positivity.Finset (1.9s)
Error: error: Mathlib/Tactic/Positivity/Finset.lean:67:2: (interpreter) unknown declaration 'Mathlib.Meta.Positivity.evalFinsetSum'
Error: error: Mathlib/Tactic/Positivity/Finset.lean:68:4: Unknown constant `Lean.throwError._at_.Lean.throwErrorAt._at_.Lean.throwUnknownIdentifierAt._at_.Lean.throwUnknownConstantAt._at_.Lean.throwUnknownConstant._at_.Lean.getConstInfo._at_.Lean.getConstInfoCtor._at_._private.Plausible.DeriveArbitrary.0.Plausible.getCtorArgsNamesAndTypes.spec_1.spec_1.spec_1.spec_1.spec_1.spec_3.spec_3`

[Damiano Testa]

Is it #mathlib4 > compilation error on master? ?

[Ruben Van de Velde]

We're dealing with some issues that might be related. I'd wait a few hours and then merge master and try again