LeanInk can't install itself for brew-installed elan
Opened this issue ยท 10 comments
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:
- 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." - 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.
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.
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
?
Eh, I would like to avoid modifying installed toolchains. By local I really meant local to the package.
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?
I guess not, but the difference between --ink ../$4/build/bin/leanInk
and PATH=../$4/build/bin:$PATH
seems superficial to me.
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 .
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
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:
require
LeanInk in the lakefile so LeanInk local to the package would be cloned and built- combine
Workspace.packagesDir
(of Lake) withLeanInk/build/bin/leanInk
to get the local LeanInk path - 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
Yes, something like that. See also leanprover/lake#80 for a discussion relating to development-only dependencies.
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
.