lake install

Stream: lean4

[Arthur Paulino]

Is there something like a lake install planned?

I tried to programmatically copy the executable binary file generated by lake build to a folder in my PATH. But the copied file no longer has permission to be executed. I remember this solution used to work in the past.

Nevertheless, a lake install (like cargo install) seems like a better solution overall.

In any case, while there's no such thing, can someone help me make the copying strategy work?

Thanks in advance!

[Julian Berman]

Does symlinking it instead work? Or otherwise maybe checking otool -L (or ldd) to see whether it's trying to look for libraries in relative paths or something might be worth checking.

[Arthur Paulino]

Symlink won't work because the original binary file is not stable. I need the real binary file to be put on a separate folder and made available to be called.

Maybe I didn't understand the otool idea, but the issue doesn't seem to be related to calls to things by relative paths. You can reproduce it with just a hello world program. The issue really is the fact that the copied file ends up without permission to be executed, while the original file created by Lake has the permission to be executed.

[Julian Berman]

It seems to work here (on macOS):

⊙  rm -rf foo ~/.local/bin/foo && lake new foo && cd foo && lake build --quiet && cp .lake/build/bin/foo ~/.local/bin && ~/.local/bin/foo                                                                                                                                                                                                                         julian@Mac
Hello, world!

What do you get?

[Arthur Paulino]

I'm not copying with cp. I'm copying with a Lean script so it can work on Windows as well.

I do this:

IO.FS.writeBinFile tgtPath (← IO.FS.readBinFile srcPath)

And when I try to execute it with ./path-to-my-bin it just says "Permission denied"

[Julian Berman]

Hm. Well let's see what that does, maybe it's not preserving the executable bit.

[Julian Berman]

I mean I guess you said already that it's not.

[Julian Berman]

So I guess let's see what the way to do that is.

[Arthur Paulino]

When I ls -lh on the original file, it says -rwxrwxr-x. But for the newly created file it says -rw-rw-r--. I've lost the xs for execution permissions

[Julian Berman]

Yeah. I see Lean has FS.setAccessRights which looks like it exposes chmod.

[Julian Berman]

I don't see stat yet

[Arthur Paulino]

But let me reiterate that I don't like this manual copying strategy, even when it works. I'd rather have a principled way to install binaries like cargo install for Rust or stack install for Haskell etc

[Julian Berman]

(nod, agree with that)

[Arthur Paulino]

Julian Berman said:

Yeah. I see Lean has FS.setAccessRights

Where is that? I type IO.FS. and that function doesn't show up for auto-completion

[Arthur Paulino]

Ah, it's IO.setAccessRights

[Julian Berman]

Sorry that, yes. (I should learn to stop trying to answer what namespace a declaration is via Cmd-F "namespace"...)

[Arthur Paulino]

Okay, that did the trick. Thanks!