Interleaved expected output in leantest_csimpAttr.lean?

[lovettchris]

Prerequisites

• [x] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

~/lean4/tests/lean/csimpAttr.lean fails on windows under MSys2.

Steps to Reproduce

Run the unit tests from stage1 with ctest -j10 -E leanlaketest_git

Expected behavior:

100% pass rate

Actual behavior:

The following tests FAILED: 188 - leantest_csimpAttr.lean (Failed) 479 - leantest_updateExprIssue.lean (Failed)

The checked in C:\msys64\home\clovett\git\lean4\tests\lean\csimpAttr.lean.expected.out has garbled interleaved output???

[init]
def f (x_1 : obj) : obj :=
  let x_2 : obj := Nat.add x_1 x_1;
  let x_3 : obj := Nat.add x_2 x_2;
  ret x_3csimpAttr.lean:7:2-7:7: error: invalid 'csimp' theorem, only constant replacement theorems (e.g., `@f = @g`) are currently supported.

but on Windows we get nice clean orderly output:

csimpAttr.lean:7:2-7:7: error: invalid 'csimp' theorem, only constant replacement theorems (e.g., `@f = @g`) are currently supported.

[init]
def f (x_1 : obj) : obj :=
  let x_2 : obj := Nat.add x_1 x_1;
  let x_3 : obj := Nat.add x_2 x_2;
  ret x_3

And leantest_updateExprIssue.lean seems to fail because on windows there is one more newline at the end of the produced output. Perhaps the comparer should strip trailing newlines?

Reproduces how often: 100%

Versions

Lean (version 4.0.0, commit e90e144eadc5, Release)

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

[Kha]

Hmm, seems to work fine in CI though?

[Kha]

The checked in C:\msys64\home\clovett\git\lean4\tests\lean\csimpAttr.lean.expected.out has garbled interleaved output???

This will probably be resolved with the new compiler

[tydeu]

@Kha

Hmm, seems to work fine in CI though?

Yes, this is true, which is why I personally never reported these errors. For me, the following tests consistently break on my Windows machine (but pass the CI):

leantest_csimpAttr.lean
leantest_updateExprIssue.lean
leancomptest_foreign
leanplugintest_SnakeLinter.lean