lean
lean copied to clipboard
Test failure on i686 (32 bit)
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.
- Specifically, check out the wishlist, open RFCs, or feature requests.
- Reduced the issue to a self-contained, reproducible test case.
- Checked that your issue isn't already filed.
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
- Build lean on 32 bit linux (specifically void linux i686)
- 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.