Verso: could not execute external process

Stream: lean4

[Utensil Song]

As my previous Alectryon/LeanInk setup failed with some Python errors, and Verso supports proof states now (:tada: :heart:), I am trying to port those Lean files to Verso.

I could not find the source of e.g. https://lean-lang.org/blog/2024-2-29-lean-460/ , so I just cloned verso and run lake build following its README and trying to fiddle with the demo site, then I got this error:

[89/100] Building DemoSite.Blog.Subprojects
error: > LEAN_PATH=./.lake/packages/subverso/.lake/build/lib:./.lake/build/lib DYLD_LIBRARY_PATH=./.lake/build/lib /Users/utensil/.elan/toolchains/leanprover--lean4---v4.7.0-rc1/bin/lean ././examples/website/DemoSite/Blog/Subprojects.lean -R ././examples/website -o ./.lake/build/lib/DemoSite/Blog/Subprojects.olean -i ./.lake/build/lib/DemoSite/Blog/Subprojects.ilean -c ./.lake/build/ir/DemoSite/Blog/Subprojects.c
error: stdout:
././examples/website/DemoSite/Blog/Subprojects.lean:24:0: error: Build process failed.
stderr:
could not execute external process '/Users/utensil/.elan/bin/lake'
error: stderr:
Build process failed.
CWD: /Users/utensil/projects/verso/examples/website-examples
Command: /Users/utensil/.elan/bin/lake
Exit code: 255
stdout:
stderr: could not execute external process '/Users/utensil/.elan/bin/lake'
error: external command `/Users/utensil/.elan/toolchains/leanprover--lean4---v4.7.0-rc1/bin/lean` exited with code 1

I'm on Mac M1 and I have no clue whether there should be a lake in .elan/bin nowadays (and how I end up having no lake in .elan/bin and how to fix it if needed), and other Lean projects seems to be working well with lake inside the toolchain specific bin/lake while verso uses .elan/bin/lake per SubVerso.Examples.findElanLake.

[Kim Morrison]

% git clone git@github.com:leanprover/verso.git
% cd verso
% lake build

is working for me.

[Kim Morrison]

I would assume your elan is broken in some way, and would suggest just deleting ~/.elan, reinstalling elan, and trying again.

[Kim Morrison]

If that fails, could you try to make an exact repro?

[Sebastian Ullrich]

@Utensil Song Is your elan from homebrew?

[Utensil Song]

Sebastian Ullrich said:

Utensil Song Is your elan from homebrew?

Yes, it was installed by brew install elan-init as instructed here.

[Utensil Song]

Scott Morrison said:

I would assume your elan is broken in some way, and would suggest just deleting ~/.elan, reinstalling elan, and trying again.

I have indeed tried this, but the same error persists. I wonder if the search priority for lake in the subverso code is optimal, since other projects successfully found a lake (in toolchain-specific bin).

[Utensil Song]

BTW, any chances the source of https://lean-lang.org/blog/2024-2-29-lean-460/ is publicly available somewhere?

[Kim Morrison]

As far as I can tell, it is generated from the private repo https://github.com/leanprover/lean-fro.org (although I don't understand which branch, if that is the correct source: master hasn't been updated for months...)

@David Thrane Christiansen?

[David Thrane Christiansen]

The reason it wants to run lake is because of newly-landed support for including code examples written in other versions of Lean. The demonstration website does this. It jumps through some hoops to avoid the toolchain-specific version, as it needs to get the Elan proxy binary in order to cross Lean versions, but this is clearly not general enough right now. I created an issue to track it. Right now, if $ELAN_HOME is set, it assumes that there's a lake proxy there - it should probably check first, and then iterate over $PATH if not. Thanks for finding this!

@Scott Morrison It is indeed that private repo, but the leandoc branch. That repo generates both our websites, and they share a fair bit of code.

The repo is private because we sometimes want to prepare something privately, e.g. in connection with job postings. This is definitely less great from the perspective of using it as an example - I'll talk over the tradeoffs with the rest of the FRO.

[Utensil Song]

Thanks for the issue and the explanations. I used the following workaround on Mac for an elan from homebrew without a ~/.elan/bin/lake:

mkdir ~/.elan/bin/
ln -s ~/.elan/toolchains/leanprover--lean4---v4.7.0-rc2/bin/lake ~/.elan/bin/lake

Then it seems to be unable to use the old Lean version as intended:

error: stdout:
././examples/website/DemoSite/Blog/Subprojects.lean:52:0: error: Didn't match - expected one of:
  ["4.7.0-rc2" ]
but got:
  "4.5.0"

I can bypass this by changing it to "4.7.0-rc2" in Lean and lake build and site generation no longer complains, but the resulting page also doesn't seem to be using the old Lean features correctly:

image.png

[Mac Malone]

David Thrane Christiansen said:

Right now, if $ELAN_HOME is set, it assumes that there's a lake proxy there - it should probably check first, and then iterate over $PATH if not. Thanks for finding this!

This sounds imilar to an issue I previously encountered with assuming elan would be located in $ELAN_HOME/bin. It now sounds like it is not safe to assume either elan or lake are in $ELAN_HOME/bin when installed via a a distro. This makes me curious what is guarenteed to be in the bin directory of ELAN_HOME, if anything. @Sebastian Ullrich, could you offer some insights as to the expected behavior/structure of ELAN_HOME?

[Sebastian Ullrich]

ELAN_HOME is the home of toolchains, not necessarily of elan's own binaries. So don't assume bin/ to exist.

[Utensil Song]

Yes, my observation after a few reinstallations is that there is no bin under ELAN_HOME at all.

which elan gives /opt/homebrew/bin/elan while which lake gives /opt/homebrew/bin/lake.

[David Thrane Christiansen]

I won't get this fixed for the next week or so - apologies! But it should work for now to symlink the Elan proxies for the Lean tools into the ELAN_HOME/bin directories, rather than the concrete toolchain that you're using.

[Utensil Song]

Aha, I see where my workaround went wrong, thanks!

EDIT: Using

ln -s `which lake` ~/.elan/bin/lake

instead, it now works like a charm!

[David Thrane Christiansen]

Good to hear!