leanprover-community / leanprover-community/lean

Test failure on i686 (32 bit)

Open
#685 0 comments 0 reactions 0 assignees View on GitHub

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.
    • 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.

Contributor guide

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. 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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.