leanprover-community / leanprover-community/lean
Test failure on i686 (32 bit)
Nobody has claimed this yet.
- Dominant language
- C++
- Stars
- 434
- Forks
- 79
- PR merge metrics
- No merged PRs in 30d
Description
Prerequisites
- 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.
- Specifically, check out the wishlist, open RFCs,
- 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.
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Reproduce the failure on Void Linux i686 by running the test suite and focus on leanittest_complete_trailing_period.lean. Compare its expected output with the produced output, then identify why completions are empty on 32-bit Linux; done means the test passes without changing behavior on supported platforms.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- cpp, linux
- Domain
- operating-systems, testing-qa
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Stale
- Clarity
- Needs clarification
- Newbie friendliness
- 35/100