LeanInk can't install itself for brew-installed elan

[utensil]

Description

LeanInk can't install itself for brew-installed elan, the error output is:

Installing LeanInk...
cp: directory /Users/[MYUSERNAME]/.elan/bin does not exist
Failed copying LeanInk to .elan/bin!

Under my .elan, ls shows:

settings.toml   tmp             toolchains      update-hashes

no sign of bin.

The elan in use is:

% ls -lhta `which elan`
[OMITTED] /usr/local/bin/elan -> ../Cellar/elan-init/1.4.1/bin/elan

Expected behaviour

LeanInk could detect if elan is intalled into ~/.elan and act accordingly such as soft-lining from /usr/local/bin/.

Reproducing the issue

# 1. Follow https://leanprover-community.github.io/install/macos.html#m1-macs--apple-silicon to install elan on M1 Macs / Apple Silicon or just `brew install elan-init` for other Macs
# 2. Install LeanInk
sh -c "$(curl https://raw.githubusercontent.com/leanprover/LeanInk/main/init.sh -sSf)"

Environment information

• Operating System: macOS Monterey 12.4 on MacBookPro (16-inch, 2021) with Apple M1 Pro
• Lean version: Lean (version 4.0.0-nightly-2022-07-10, commit 23bae264fd1f, Release)
• LeanInk version: Latest commit: 4b5e606
• Alectryon version: N/A

Suggested fix

Two options:

1. Fix the line ELAN_BIN="$HOME/.elan/bin/" in https://github.com/leanprover/LeanInk/blob/main/install.sh that assumes "that lean is already installed as expected we can assume that the .elan folder already exists and is correctly linked."
2. Fix https://github.com/Homebrew/homebrew-core/blob/HEAD/Formula/elan-init.rb to add symlink for ~/.elan as well

1 is more pratical.

Additional Notes

I've bypassed the issue by following https://github.com/leanprover/LeanInk#building-from-source and manually copy leanInk to /usr/local/bin which seems to be working fine.

[Kha]

I'm not sure if it even makes sense to keep the installation script. As LeanInk is very sensitive to the used Lean version, it makes much more sense as a local (dev) dependency of a package.

[utensil]

I'm not sure if it even makes sense to keep the installation script. As LeanInk is very sensitive to the used Lean version, it makes much more sense as a local (dev) dependency of a package.

Then the proper fix could be: add installation to lakefile and install LeanInk into ~/.elan/toolchains/[WHERE THE CURRENT LEAN IS INSTALLED]/bin?

[Kha]

Eh, I would like to avoid modifying installed toolchains. By local I really meant local to the package.

[utensil]

I see, like the usage in https://github.com/leanprover/doc-gen4/blob/main/deploy_docs.sh#L26 : --ink ../$4/build/bin/leanInk.

But in the doc of https://github.com/cpitclaudel/alectryon, there's no argument to specify where LeanInk is, so it still need to be on the PATH somewhere or have I missed something?

[Kha]

I guess not, but the difference between --ink ../$4/build/bin/leanInk and PATH=../$4/build/bin:$PATH seems superficial to me.

[utensil]

Yes, it's superficial for a developer, but not so for an end user who could be using alectryon to literate lean authoring.

I've checked the source of alectryon, there's no way to specify where LeanInk is (i.e. nothing like --ink), it's completely up to the user to setup a working LeanInk in PATH. Meanwhile, why docgen4 works fine is because it's using LeanInk directly (so it has its own --ink flag) and some alectryon assets and the corresponding HTML in source: https://github.com/leanprover/doc-gen4/blob/3924034385bf6feea1a40e9281542e1a88fdff7f/DocGen4/LeanInk/Output.lean#L178 .

[Kha]

I've checked the source of alectryon, there's no way to specify where LeanInk is (i.e. nothing like --ink)

That does sound like a worthwhile addition you could create an issue for

[utensil]

Eh, I would like to avoid modifying installed toolchains. By local I really meant local to the package.

After a closer look at doc-gen4 ( the lakefile in particular ), now I see what you mean could actually be:

1. require LeanInk in the lakefile so LeanInk local to the package would be cloned and built
2. combine Workspace.packagesDir (of Lake) with LeanInk/build/bin/leanInk to get the local LeanInk path
3. invoke LeanInk found in step 2, or invoke alectryon with a PATH that has the local LeanInk path or a flag like --ink refering to the local LeanInk path

[Kha]

Yes, something like that. See also leanprover/lake#80 for a discussion relating to development-only dependencies.

[lovettchris]

I've removed the troublesome install script in this PR: #31 and ported the run tests script to lakefile.lean so you can now run lake script run tests.