Zulip Chat Archive

Stream: nightly-testing

Topic: nanoda failure

github mathlib4 bot (Jan 08 2026 at 00:47):

:cross_mark: nanoda failure on d07aaeafc78bf4d5df7ed728fd92f9f48fe0b7be (branch: master)

github mathlib4 bot (Jan 08 2026 at 00:48):

:cross_mark: nanoda failure on d07aaeafc78bf4d5df7ed728fd92f9f48fe0b7be (branch: nightly-testing-2026-01-07)

Kim Morrison (Jan 08 2026 at 01:27):

First strangeness: when clicking through to the logs, the nanoda run on master was actually fine, but the bot reported it failed too.

Bryan Gin-ge Chen (Jan 08 2026 at 01:48):

I'll take a look, my guess is there's something wrong with the link in the workflow.

Bryan Gin-ge Chen (Jan 08 2026 at 02:00):

Fixed in #33738, hopefully

Bryan Gin-ge Chen (Jan 08 2026 at 03:38):

I've manually triggered daily.yml to check to see if the fix really worked.

github mathlib4 bot (Jan 08 2026 at 04:05):

:cross_mark: nanoda failure on c627e665ea632256d0c5708f43f1541739c169eb (branch: nightly-testing-2026-01-07)

Kim Morrison (Jan 08 2026 at 04:21):

Looks good. I am busy trying to work out why nanoda is actually failing on nightly-testing right now. (@Chris Bailey, just pinging you for awareness that we're working on this.)

Chris Bailey (Jan 08 2026 at 05:09):

Looking at the failure and the branch being used it's almost certainly because it doesn't implement the special case handling for eagerReduce.

Chris Bailey (Jan 08 2026 at 05:13):

The README (on master) notes that it's temporarily broken until the JSON stuff gets merged. The json_string branch has both the json parsing and the upstream kernel changes. I can merge the eager reduction stuff into debug if this failure is blocking anything, but that branch was not necessarily meant to be used for anything other than observing the failures caused by the identifier issue and the kernel changes before I was aware of them. The handling for identifiers with white spaces is a hack and is not technically not correct; it would have required a total rewrite of the parser for a format that we knew was on the way out.

Kim Morrison (Jan 08 2026 at 05:28):

Okay. Very happy to follow your lead here; if we simply shouldn't run nanoda against nightly-testing for a while (or just ignore the failures) that's okay.

But let me know if there's something I can test/help with, as I'm very keen to get to the point we're successfully running nanoda every day on both!

Kim Morrison (Jan 08 2026 at 05:31):

(re: the white space in identifiers, I don't know if you saw batteries#1601, which should give us some breathing room)

github mathlib4 bot (Jan 09 2026 at 00:47):

:cross_mark: nanoda failure on ee6d0f13b3a203fa0701998900d057484a769679 (branch: nightly-testing-2026-01-08)

github mathlib4 bot (Jan 10 2026 at 00:45):

:cross_mark: nanoda failure on b8e3880e7aebc634d9d78b14d1fc00a25b299ea0 (branch: nightly-testing-2026-01-09)

github mathlib4 bot (Jan 11 2026 at 00:50):

:cross_mark: nanoda failure on c2ac49c165a4c4075c4716ea2deb90b594b6900a (branch: nightly-testing-2026-01-10)

github mathlib4 bot (Jan 12 2026 at 00:50):

:cross_mark: nanoda failure on 622f41abb60ba23b0c4866b6ebb75a5629932070 (branch: nightly-testing-2026-01-11)

github mathlib4 bot (Jan 13 2026 at 00:43):

:cross_mark: nanoda failure on c1d772d6329adbf19893119c31cea6c4127420e7 (branch: nightly-testing-2026-01-12)

github mathlib4 bot (Jan 14 2026 at 00:48):

:cross_mark: nanoda failure on 26e1e450e24367d8b4b4662157d75eda0f6336ef (branch: nightly-testing-2026-01-12)

github mathlib4 bot (Jan 15 2026 at 00:49):

:cross_mark: nanoda failure on 79a359dfe4682c5ca375c39522d7c64e95659d5a (branch: nightly-testing-2026-01-14)

github mathlib4 bot (Jan 16 2026 at 00:48):

:cross_mark: nanoda failure on 986dfcf2d26d0373b1a1a38ee2a8764ca90a0cb4 (branch: nightly-testing-2026-01-14)

github mathlib4 bot (Jan 17 2026 at 00:48):

:cross_mark: nanoda failure on 20b873c44e11e4e3c5c39c5d10f2096053ccf8a5 (branch: nightly-testing-2026-01-14)

github mathlib4 bot (Jan 18 2026 at 00:48):

:cross_mark: nanoda failure on 5c74f14cc87eb3a97d3e9cd058487f1d9571c3ab (branch: nightly-testing-2026-01-14)

github mathlib4 bot (Jan 19 2026 at 00:47):

:cross_mark: nanoda failure on 7048ffa529b90841dce5015ed4cc61e7fd5d7261 (branch: nightly-testing-2026-01-14)

github mathlib4 bot (Jan 20 2026 at 00:48):

:cross_mark: nanoda failure on d0871e12f31a4e24ed78a6c09dfb32c4f625d6a9 (branch: nightly-testing-2026-01-14)

github mathlib4 bot (Jan 21 2026 at 00:49):

:cross_mark: nanoda failure on 06cfbfe1a8469cbcbc221717bafa6b38132961de (branch: nightly-testing-2026-01-20)

github mathlib4 bot (Jan 22 2026 at 00:49):

:cross_mark: nanoda failure on 9ffe92940ecaeb3dcd538bc6e1644e60c32d4561 (branch: nightly-testing-2026-01-21)

github mathlib4 bot (Jan 23 2026 at 00:49):

:cross_mark: nanoda failure on 725d7a32b7cbbb51127cacb581d40dacc6be6b52 (branch: nightly-testing-2026-01-22)

github mathlib4 bot (Jan 24 2026 at 00:49):

:cross_mark: nanoda failure on 4c87e1d930d0fa219f001b56130c99e32d84fc26 (branch: nightly-testing-2026-01-23)

github mathlib4 bot (Jan 25 2026 at 00:51):

:cross_mark: nanoda failure on be04ab25ca4157be69980ea7f908c865738b7388 (branch: nightly-testing-2026-01-24)

github mathlib4 bot (Jan 26 2026 at 00:51):

:cross_mark: nanoda failure on 168b9cff12dab685d3df073d0327ad4bb75843d3 (branch: nightly-testing-2026-01-25)

github mathlib4 bot (Jan 27 2026 at 00:35):

:cross_mark: nanoda failure on cbf90bf1c877113a9bea3e3bd2fe2c8e0ed1325b (branch: master)

github mathlib4 bot (Jan 27 2026 at 00:35):

:cross_mark: nanoda failure on cbf90bf1c877113a9bea3e3bd2fe2c8e0ed1325b (branch: nightly-testing-2026-01-25)

Kim Morrison (Jan 27 2026 at 04:41):

Hmm, nanoda is now also failing on master now that we've moved to v4.28.0-rc1.

Kim Morrison (Jan 27 2026 at 04:41):

Is anyone interested in investigating here?

github mathlib4 bot (Jan 27 2026 at 10:42):

:cross_mark: nanoda failure on 002831b4f30ea1bb23e788d8517426d32b0538f6 (branch: master)

github mathlib4 bot (Jan 27 2026 at 10:43):

:cross_mark: nanoda failure on 002831b4f30ea1bb23e788d8517426d32b0538f6 (branch: nightly-testing-2026-01-27)

github mathlib4 bot (Jan 28 2026 at 00:33):

:cross_mark: nanoda failure on ed96f50f75b1f89c4561f2ba2d837eb169052094 (branch: master)

github mathlib4 bot (Jan 28 2026 at 00:34):

:cross_mark: nanoda failure on ed96f50f75b1f89c4561f2ba2d837eb169052094 (branch: nightly-testing-2026-01-27)

github mathlib4 bot (Jan 29 2026 at 00:37):

:cross_mark: nanoda failure on 426f4b033ae682c66dfc327f6c3717569786ae9e (branch: master)

github mathlib4 bot (Jan 29 2026 at 00:37):

:cross_mark: nanoda failure on 426f4b033ae682c66dfc327f6c3717569786ae9e (branch: nightly-testing-2026-01-28)

github mathlib4 bot (Jan 30 2026 at 00:45):

:cross_mark: nanoda failure on 62a82d6d0a3d3c54ca96bf00a861c623f3e0be44 (branch: master)

github mathlib4 bot (Jan 30 2026 at 00:46):

:cross_mark: nanoda failure on 62a82d6d0a3d3c54ca96bf00a861c623f3e0be44 (branch: nightly-testing-2026-01-28)

github mathlib4 bot (Jan 31 2026 at 00:37):

:cross_mark: nanoda failure on 0ecfe98f64977839ba2ae6a5ed4c96e026c6d995 (branch: master)

github mathlib4 bot (Jan 31 2026 at 00:37):

:cross_mark: nanoda failure on 0ecfe98f64977839ba2ae6a5ed4c96e026c6d995 (branch: nightly-testing-2026-01-30)

Joachim Breitner (Jan 31 2026 at 09:22):

Kim Morrison schrieb:

Hmm, nanoda is now also failing on master now that we've moved to v4.28.0-rc1.

@Chris Bailey

github mathlib4 bot (Feb 01 2026 at 00:41):

:cross_mark: nanoda failure on c3cf7cbc7d8787edab1c190e3b1cf48941d4854c (branch: master)

github mathlib4 bot (Feb 01 2026 at 00:41):

:cross_mark: nanoda failure on c3cf7cbc7d8787edab1c190e3b1cf48941d4854c (branch: nightly-testing-2026-01-31)

Kim Morrison (Feb 01 2026 at 11:58):

@Chris Bailey @Joachim Breitner I'm not certain what the best channel/venue to discuss nanoda is. I have some local patches that seem reasonable to get nanoda checking lean Init at v4.28.0-rc1, but I'm failing at Char.toUpper._proof_1 in Init/Data/Char/Basic.lean:

  @[inline]
  def toUpper (c : Char) : Char :=
    if h : c.val ≥ 'a'.val ∧ c.val ≤ 'z'.val then
      ⟨c.val + ('A'.val - 'a'.val), ?_⟩
    else
      c
  where finally
    have h₁ : 2^32 ≤ c.val.toNat + ('A'.val - 'a'.val).toNat :=
      @Nat.add_le_add 'a'.val.toNat _ (2^32 - 'a'.val.toNat) _ h.1 (by decide)
    have h₂ : c.val.toBitVec.toNat + ('A'.val - 'a'.val).toNat < 2^32 + 0xd800 :=
      Nat.add_lt_add_right (Nat.lt_of_le_of_lt h.2 (by decide)) _
    have add_eq {x y : UInt32} : (x + y).toNat = (x.toNat + y.toNat) % 2^32 := rfl
    replace h₂ := Nat.sub_lt_left_of_lt_add h₁ h₂
    exact .inl <| lt_of_eq_of_lt (add_eq.trans (Nat.mod_eq_sub_mod h₁) |>.trans
      (Nat.mod_eq_of_lt (Nat.lt_trans h₂ (by decide)))) h₂

Joachim Breitner (Feb 01 2026 at 12:09):

Maybe we need a #external checkers channel? Although this may best be an issue on the repo? I should Chris say what works best for him

Chris Bailey (Feb 01 2026 at 19:26):

Kim Morrison said:

Chris Bailey Joachim Breitner I'm not certain what the best channel/venue to discuss nanoda is. I have some local patches that seem reasonable to get nanoda checking lean Init at v4.28.0-rc1, but I'm failing at Char.toUpper._proof_1 in Init/Data/Char/Basic.lean:

  @[inline]
  def toUpper (c : Char) : Char :=
    if h : c.val ≥ 'a'.val ∧ c.val ≤ 'z'.val then
      ⟨c.val + ('A'.val - 'a'.val), ?_⟩
    else
      c
  where finally
    have h₁ : 2^32 ≤ c.val.toNat + ('A'.val - 'a'.val).toNat :=
      @Nat.add_le_add 'a'.val.toNat _ (2^32 - 'a'.val.toNat) _ h.1 (by decide)
    have h₂ : c.val.toBitVec.toNat + ('A'.val - 'a'.val).toNat < 2^32 + 0xd800 :=
      Nat.add_lt_add_right (Nat.lt_of_le_of_lt h.2 (by decide)) _
    have add_eq {x y : UInt32} : (x + y).toNat = (x.toNat + y.toNat) % 2^32 := rfl
    replace h₂ := Nat.sub_lt_left_of_lt_add h₁ h₂
    exact .inl <| lt_of_eq_of_lt (add_eq.trans (Nat.mod_eq_sub_mod h₁) |>.trans
      (Nat.mod_eq_of_lt (Nat.lt_trans h₂ (by decide)))) h₂

This is probably going to be very unpleasant to debug. The pp.analyze version of this proof throws a "maximum recursion depth reached" error in vscode: link.

The stack overflow occurs in a def eq obligation: 

  ((c.val + ('A'.val - 'a'.val)).toNat =
      (c.val + ('A'.val - 'a'.val)).toNat) =
    ((c.val + ('A'.val - 'a'.val)).toNat =
      (c.val.toNat + ('A'.val - 'a'.val).toNat) % OfNat.ofNat 2 ^ OfNat.ofNat 32)

Which gives a kernel deep recursion detected error in vscode. Maybe toUpper is able to get away with this because it has add_eq as a local, which replaces the concrete values with free variables and is therefore def eq without blowing the stack, if I remember correctly upstream has some fancier handling of let bindings or something. With the amount of computation that's been offloaded onto the kernel it seems like there's very little room for any deviation from the imperative flow or reducibility optimizations used by the C++ implementation.

Robin Arnez (Feb 01 2026 at 19:52):

Well, I'm responsible for this... does this work?

@[inline]
def toUpper (c : Char) : Char :=
  if h : 'a'.val ≤ c.val ∧ c.val ≤ 'z'.val then
    ⟨c.val + ('A'.val - 'a'.val), ?_⟩
  else
    c
where finally
  have le_def {x y : UInt32} : (x ≤ y) = (x.toNat ≤ y.toNat) := rfl
  have add_eq {x y : UInt32} : (x + y).toNat = (x.toNat + y.toNat) % 2^32 := rfl
  rw [le_def, le_def] at h
  have h₁ : 2^32 ≤ c.val.toNat + ('A'.val - 'a'.val).toNat := by
    rw [← Nat.sub_add_cancel (show 'a'.val.toNat ≤ 2^32 by decide), Nat.add_comm]
    exact @Nat.add_le_add 'a'.val.toNat _ (2^32 - 'a'.val.toNat) _ h.1 (by decide)
  have h₂ : c.val.toNat + ('A'.val - 'a'.val).toNat < 2^32 + 0xd800 := by
    apply Nat.add_lt_of_lt_sub
    exact Nat.lt_of_le_of_lt h.2 (by decide)
  replace h₂ := Nat.sub_lt_left_of_lt_add h₁ h₂
  rw [UInt32.isValidChar, Nat.isValidChar]
  exact .inl <| lt_of_eq_of_lt (add_eq.trans (Nat.mod_eq_sub_mod h₁) |>.trans
    (Nat.mod_eq_of_lt (Nat.lt_trans h₂ (by decide)))) h₂

I've tested that the proof type-checks under reducible transparency

Joachim Breitner (Feb 01 2026 at 20:41):

@Kim Morrison , before blaming nanoda, do we have a successful run of leanchecker in --fresh mode? Because if not it may be due to the module system, where the per-module checks go through but the --fresh mode fails with the official kernel as well because something is now transparent?

github mathlib4 bot (Feb 02 2026 at 00:38):

:cross_mark: nanoda failure on 69decbd50b5e6926d418b3c1f3c58e868c45a382 (branch: master)

github mathlib4 bot (Feb 02 2026 at 00:39):

:cross_mark: nanoda failure on 69decbd50b5e6926d418b3c1f3c58e868c45a382 (branch: nightly-testing-2026-02-01)

Kim Morrison (Feb 02 2026 at 10:01):

Joachim Breitner said:

Kim Morrison , before blaming nanoda, do we have a successful run of leanchecker in --fresh mode? Because if not it may be due to the module system, where the per-module checks go through but the --fresh mode fails with the official kernel as well because something is now transparent?

Yes, these runs are running leanchecker --fresh.

github mathlib4 bot (Feb 03 2026 at 00:38):

:cross_mark: nanoda failure on 6a1be3670f0ce93db58a5e948851abd5d9b751b3 (branch: master)

github mathlib4 bot (Feb 03 2026 at 00:39):

:cross_mark: nanoda failure on 6a1be3670f0ce93db58a5e948851abd5d9b751b3 (branch: nightly-testing-2026-02-02)

github mathlib4 bot (Feb 04 2026 at 00:35):

:cross_mark: nanoda failure on be8defd50c175d2ce7598a43c1be199f53b7cae6 (branch: master)

github mathlib4 bot (Feb 04 2026 at 00:36):

:cross_mark: nanoda failure on be8defd50c175d2ce7598a43c1be199f53b7cae6 (branch: nightly-testing-2026-02-02)

github mathlib4 bot (Feb 05 2026 at 00:37):

:cross_mark: nanoda failure on ba07a5d5fb83488d3accc0fe05f0c1fbca22bda4 (branch: master)

github mathlib4 bot (Feb 05 2026 at 00:38):

:cross_mark: nanoda failure on ba07a5d5fb83488d3accc0fe05f0c1fbca22bda4 (branch: nightly-testing-2026-02-03)

github mathlib4 bot (Feb 06 2026 at 00:36):

:cross_mark: nanoda failure on b94b918e1fd0293f3ef9c2567dfe3774f273dced (branch: master)

github mathlib4 bot (Feb 06 2026 at 00:36):

:cross_mark: nanoda failure on b94b918e1fd0293f3ef9c2567dfe3774f273dced (branch: nightly-testing-2026-02-04)

github mathlib4 bot (Feb 07 2026 at 00:37):

:cross_mark: nanoda failure on 7091f0f601d5aaea565d2304c1a290cc8af03e18 (branch: master)

github mathlib4 bot (Feb 07 2026 at 00:38):

:cross_mark: nanoda failure on 7091f0f601d5aaea565d2304c1a290cc8af03e18 (branch: nightly-testing-2026-02-05)

github mathlib4 bot (Feb 08 2026 at 00:46):

:cross_mark: nanoda failure on 668a53718f830a40e2f19d7a81515e8e60b8915f (branch: master)

github mathlib4 bot (Feb 08 2026 at 00:46):

:cross_mark: nanoda failure on 668a53718f830a40e2f19d7a81515e8e60b8915f (branch: nightly-testing-2026-02-05)

github mathlib4 bot (Feb 09 2026 at 00:39):

:cross_mark: nanoda failure on 26e91fab26eda350d9dc8147cdfa12b3e6e33a64 (branch: master)

github mathlib4 bot (Feb 09 2026 at 00:40):

:cross_mark: nanoda failure on 26e91fab26eda350d9dc8147cdfa12b3e6e33a64 (branch: nightly-testing-2026-02-05)

github mathlib4 bot (Feb 10 2026 at 00:43):

:cross_mark: nanoda failure on 5086678147029ce3164ce2033fe5d2425e3353fd (branch: master)

github mathlib4 bot (Feb 10 2026 at 00:43):

:cross_mark: nanoda failure on 5086678147029ce3164ce2033fe5d2425e3353fd (branch: nightly-testing-2026-02-08)

github mathlib4 bot (Feb 11 2026 at 00:43):

:cross_mark: nanoda failure on b8dad038b1b3a05b77d6884b15b8db03ec01dca1 (branch: master)

github mathlib4 bot (Feb 11 2026 at 00:43):

:cross_mark: nanoda failure on b8dad038b1b3a05b77d6884b15b8db03ec01dca1 (branch: nightly-testing-2026-02-10)

github mathlib4 bot (Feb 12 2026 at 00:37):

:cross_mark: nanoda failure on ea886ccefe95c2432d0a138fcc00a7c09e518b45 (branch: master)

github mathlib4 bot (Feb 12 2026 at 00:38):

:cross_mark: nanoda failure on ea886ccefe95c2432d0a138fcc00a7c09e518b45 (branch: nightly-testing-2026-02-10)

github mathlib4 bot (Feb 13 2026 at 00:39):

:cross_mark: nanoda failure on c72b0ec47221dd152064b8ad478bf3a18913b1b6 (branch: master)

github mathlib4 bot (Feb 13 2026 at 00:40):

:cross_mark: nanoda failure on c72b0ec47221dd152064b8ad478bf3a18913b1b6 (branch: nightly-testing-2026-02-10)

github mathlib4 bot (Feb 14 2026 at 00:55):

:cross_mark: nanoda failure on 738faa552745fad46e80382d1249522aa3caf0c8 (branch: master)

github mathlib4 bot (Feb 15 2026 at 00:58):

:cross_mark: nanoda failure on 88bb6d226a47fbd02dbda6e58822db638b58af5f (branch: master)

github mathlib4 bot (Feb 16 2026 at 00:54):

:cross_mark: nanoda failure on 854dbeb28ad8731d29fd6f93d82a3b960115fa60 (branch: master)

github mathlib4 bot (Feb 17 2026 at 00:57):

:cross_mark: nanoda failure on 32fe3f9354729a268ba178d0b5ae06eca180c247 (branch: master)

Last updated: Feb 28 2026 at 14:05 UTC