Installed binaries of lean-4.14.0-linux do not work #6392
Labels
bug
Something isn't working
Comments
|
I am on GNU/Guix, if that matters, running upstream Linux of 6.11.10 |
|
The binaries do work on hundreds of Linux machines so the Guix part is likely the culprit here. What does |
Maybe, but Guix is just another GNU/Linux distribution, so what could be the culprit?
|
|
Okay that looks acceptable, can you run: and show us the output of As to what the culprit could be, this error does not mean that "the binary isn't detected", it usually means that something in the early initialization of the process is going wrong. The most likely reason here is that it is looking for some shared object and not finding it. The reason that this might be is that of course Guix has a non standard layout for everything so while it might have the specific file that the binary is looking for somewhere, it might not have it in the right location. |
|
This is the output in |
|
Okay so it fails even before starting to play with shared objects, |
|
Here's the entire output, and indeed it does have a request for the interpreter: |
|
I'm gonna go ahead and guess that |
|
It does though, as |
|
Right, then something with my understanding of how the system works here is wrong. The so unless there is another condition present which is not documented in the manpage the ELF interpreter must be at fault here. One thing we could try to be sure that it is not Guix messing up the elf interpreter is to run and observing whether this still errors and in particular if it does still error, observe in |
|
Oh, @hargoniX the |
|
It sounds to me that debugging this requires guix specific knowledge. @divyaranjan1905 have you already tried getting help on guix channels? I would assume it's a common problem when running non-guix specific binaries on guix. |
|
@nomeata Hello, I can surely do. I do have knowledge of how Guix works, I am just unsure as to what exactly the binary might be looking for. Is it that the binary can't set |
|
Patching the binaries with |
|
The nix guys have a patched |
The problem is, Guix doesn't encourage packaging anything that's based on pre-built binaries. It can be done, but probably not in the official repository. I might make a separate channel for this, thanks for the debugging anyways. It was helpful. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Prerequisites
Please put an X between the brackets as you perform the following steps:
https://github.com/leanprover/lean4/issues
Avoid dependencies to Mathlib or Batteries.
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
Downloading the latest 4.14 release, unzipping and executing the binaries does not work as expected.
Steps to Reproduce
bindirectory../lean, and you'll get:zsh: no such file or directory: ./leanExpected behavior: Lean should run and show the version of 4.14
Actual behavior: The binary does not run and isn't detected.
Versions
Lean 4.1.4.0
Target: x86_64-unknown-linux-gnu
Additional Information
Here's what I went through in my terminal:
The text was updated successfully, but these errors were encountered: