lean icon indicating copy to clipboard operation
lean copied to clipboard

Test failure on i686 (32 bit)

Open tornaria opened this issue 3 years ago • 0 comments

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

On void linux i686 (32 bit) the test suite has one failure:

1352/1426 Test #1352: leanittest_complete_trailing_period.lean ....................***Failed    0.03 sec
--- complete_trailing_period.lean.expected.out	2022-02-17 13:25:34.000000000 +0000
+++ complete_trailing_period.lean.produced.out	2022-02-18 22:46:58.052805145 +0000
@@ -1,2 +1,2 @@
 {"message":"file invalidated","response":"ok","seq_num":0}
-{"completions":[{"source":,"text":"foo.rec","type":"Π (motive : foo → Sort l) (n : foo), motive n"},{"source":{"column":10,"line":3},"text":"foo.rec_on","type":"Π (motive : foo → Sort l) (n : foo), motive n"},{"source":{"column":10,"line":3},"text":"foo","type":"Type"}],"prefix":"foo.","response":"ok","seq_num":6}
+{"completions":[],"prefix":"foo.","response":"ok","seq_num":6}
ERROR: file complete_trailing_period.lean.produced.out does not match complete_trailing_period.lean.expected.out

Steps to Reproduce

  1. Build lean on 32 bit linux (specifically void linux i686)
  2. Run tests

See: https://github.com/void-linux/void-packages/pull/32559#issuecomment-902295295

Note the last link is about an old build for lean-3.32.1, but the report above was done with current lean-3.39.2.

Expected behavior: All tests pass.

Actual behavior: One test fails.

Reproduces how often: Every time.

Versions

You can get this information from copy and pasting the output of lean --version, please include the OS and what version of the OS you're running.

3.39.2, also 3.32.1

Additional Information

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

tornaria avatar Feb 19 '22 21:02 tornaria