Porting Lean

Software Ports
1

Lean is a theorem prover and programming language.

I like writing proofs, so I tried to port Lean to Haiku. Here’s the progress so far (as haikuporter package): GitHub - suhr/haikuports at lean

C++ code seems to compile. But build fails with /usr/bin/env: No such file or directory even though I replaces all occurrences of /usr/bin/env with /bin/.

Here’s the build log: gist:d1abd933e92b0d34aa2d392d30dfc35e · GitHub

While I’ll try to investigate this problem later, maybe someone else also would like to take a look?

2

“/usr/bin/env” is a tool that is often used in shellscript shebang lines to call the “right” location for a tool, when you don’t know where it is on the distro.

So for example the shebang line may be “#!/usr/bin/env bash”
Of course this isn’t really portable either, some OSes simply don’t have this tool at that location… iirc haiku is supposed to have some workaround but it does not seem to work for you here.

Anyway the solution is to just remove it entirely. If the shebang line was “#!/usr/bin/env bash” change it to “#!bash”

3

As I said, I already removed /usr/bin/env everywhere, but build still fails. So maybe somewhere /usr/bin/env is expressed in a less direct way.

4

The weird thing it the code everywhere uses usr as a part of paths. So I have no idea where this /usr comes from.

5

Quick check reveals missing package for cadical, tried building it in Terminal but not going to hunt it further down, need libnetwork but for some reason doesn’t seem to work.

/usr/bin/env should work:

6

My commit also adds this package.

1 Like
7

The env worling in shebangs is a kind of hack, because we don’t have a /usr, as a consequence it works only in shebangs. If your project somehow tries to call “/usr/bin/env” on it’s own that will fail

8

My bad :slight_smile: OK, first comment, for cadicad, add a section for the static library (should be in _devel together with the headers).
Missing TEST() case, 2 test failing/crashing, disabling them in the api/run.sh file succeeds which is pretty good. Failing tests are: parcompwrite and cfreeze.

EDIT: missing cmd:awk also in this recipe (BUILD_PREREQUIRES).

9

I just symlinked /usr/bin to /bin in haikuporter and have got a lot further in building Lean. I pushed a new commit in the lean branch.

Build still fails though because for some reason it can’t link Lake. See the build log: gist:0ac9b2e68294298aac5391abf991da09 · GitHub

Lake is a part of Lean and not an external dependency, so it’s strange that it fails to link.

10

Progressing indeed, still a few files probably need patching in: /stage0/src/runtime/

Same output here, no idea on the undefined references at the end while linking.

11

Back to the /usr/bin/envissue…

Yep, the runtime loader changes the path for shebangs, so there’s no need to patch those. In fact, was that the issue, the error message would be different:

/var/shared_memory> cat test
#!/usr/bin/missing
/var/shared_memory> ./test
runtime_loader: Cannot open file /bin/missing (needed by <NULL>): No such file or directory

No such luxury when you directly call the program, as you are asking for a path that does not exist:

~/src/haikuports> /usr/bin/env
bash: /usr/bin/env: No such file or directory

And that’s what you are getting.

There’s a hint of where it comes from just after the error:

make[7]: *** [/sources/lean4-4.21.0/build/stage0/bin/../share/lean/lean.mk:153: ../../build/stage0/lib/lean/libInit.a] Error 127

And indeed:

~/src/haikuports> grep -Fr 'usr/bin' dev-lang/lean/work-4.21.0/sources/lean4-4.2
1.0/build/
dev-lang/lean/work-4.21.0/sources/lean4-4.21.0/build/stage0/bin/leanmake:#!/usr/bin/env bash
dev-lang/lean/work-4.21.0/sources/lean4-4.21.0/build/stage0/leanc.sh:#!/usr/bin/env bash
dev-lang/lean/work-4.21.0/sources/lean4-4.21.0/build/stage0/share/lean/lean.mk:SHELL = /usr/bin/env bash -euo pipefail

That one comes from the unpatched stage0/src/lean.mk.in, not src/lean.mk.in.