MathlibTest.order error

Stream: mathlib4

[Violeta Hernández]

Can someone please explain why my PR #30482 fails to build? The error is that some example in MathlibTest.order fails with an error that isn't exactly the same as the error that it's supposed to give? I can't really tell what's going on nor what caused it.

[Violeta Hernández]

Here's the exact error:

✖ [7429/7458] Building MathlibTest.order (3.2s)
Error: error: MathlibTest/order.lean:128:2: No contradiction found.

Additional diagnostic information may be available using the `set_option trace.order true` command.
info: MathlibTest/order.lean:128:2: [order] Working on type α (partial order)
[order] Collected atoms:
    #0 := a ⊓ (b ⊔ c)
    #1 := a
    #2 := b ⊔ c
    #3 := b
    #4 := c
    #5 := a ⊓ b ⊔ a ⊓ c
    #6 := a ⊓ b
    #7 := a ⊓ c
[order] Collected facts:
    #3 ≤ #2
    #4 ≤ #2
    #2 := #3 ⊔ #4
    #0 ≤ #1
    #0 ≤ #2
    #0 := #1 ⊓ #2
    #6 ≤ #1
    #6 ≤ #3
    #6 := #1 ⊓ #3
    #7 ≤ #1
    #7 ≤ #4
    #7 := #1 ⊓ #4
    #6 ≤ #5
    #7 ≤ #5
    #5 := #6 ⊔ #7
    #0 ≠ #5
    ¬ #0 < #5
[order] Working on type ℕ (linear order)
[order] Collected atoms:
    #0 := x
    #1 := y
[order] Collected facts:
    #0 ≠ #1
    #0 ≤ #1
Error: error: MathlibTest/order.lean:126:0: ❌️ Docstring on `#guard_msgs` does not match generated message:

  error: No contradiction found.

  Additional diagnostic information may be available using the `set_option trace.order true` command.
  ---
- trace: [order] Working on type ℕ (linear order)
+ trace: [order] Working on type α (partial order)
  [order] Collected atoms:
-     #0 := x
-     #1 := y
- [order] Collected facts:
-     #0 ≠ #1
-     #0 ≤ #1
- [order] Working on type α (partial order)
- [order] Collected atoms:
      #0 := a ⊓ (b ⊔ c)
      #1 := a
      #2 := b ⊔ c
      #3 := b
      #4 := c
      #5 := a ⊓ b ⊔ a ⊓ c
      #6 := a ⊓ b
      #7 := a ⊓ c
  [order] Collected facts:
      #3 ≤ #2
      #4 ≤ #2
      #2 := #3 ⊔ #4
      #0 ≤ #1
      #0 ≤ #2
      #0 := #1 ⊓ #2
      #6 ≤ #1
      #6 ≤ #3
      #6 := #1 ⊓ #3
      #7 ≤ #1
      #7 ≤ #4
      #7 := #1 ⊓ #4
      #6 ≤ #5
      #7 ≤ #5
      #5 := #6 ⊔ #7
      #0 ≠ #5
      ¬ #0 < #5
+ [order] Working on type ℕ (linear order)
+ [order] Collected atoms:
+     #0 := x
+     #1 := y
+ [order] Collected facts:
+     #0 ≠ #1
+     #0 ≤ #1
error: Lean exited with code 1

[Violeta Hernández]

I think all that really happened was that the messages got rearranged? Is the test non-deterministic? Seems like a bad test if so.

[Bhavik Mehta]

@Vasilii Nesterov might have an idea here

[Vasilii Nesterov]

Yes, the order in which types are printed here is arbitrary, and changes in the imports of order.lean can change this order. I realized it only after this test got merged. I delete the second type from the test in #30510.

[Vasilii Nesterov]

The right thing to do is to test the output up to permutation, but we don't have a tool for it