install leanprover/lean4 again and again

[wieniawski-lai]

hi,

I have installed lean4 manually using elan-init.sh.

And I have set enviroment variable on linux

export ELAN_HOME=/opt/elan
export PATH=$ELAN_HOME/bin:$PATH

And I also downloaded toolchains from lean4, including version 4.33 and 4.30. Both the 2 versions are un-archeived to /top/elan/toolchains. And I can see they can be found by elan toolchain list:

It seems that my env-var and installation are successful.

However, when I open VSCode with Lean 4 extension installed, and open the cloned mathematics_in_learn. it start to down load and install lean-4.30.0-linux.tar.zst again. The log is shown below:

/home/schoenberg/work/study/lean/mathematics_in_lean> curl --version
curl 7.81.0 (x86_64-pc-linux-gnu) libcurl/7.81.0 OpenSSL/3.0.2 zlib/1.2.11 brotli/1.0.9 zstd/1.4.8 libidn2/2.3.2 libpsl/0.21.0 (+libidn2/2.3.2) libssh/0.9.6/openssl/zlib nghttp2/1.43.0 librtmp/2.3 OpenLDAP/2.5.18
Release-Date: 2022-01-05
Protocols: dict file ftp ftps gopher gophers http https imap imaps ldap ldaps mqtt pop3 pop3s rtmp rtsp scp sftp smb smbs smtp smtps telnet tftp 
Features: alt-svc AsynchDNS brotli GSS-API HSTS HTTP2 HTTPS-proxy IDN IPv6 Kerberos Largefile libz NTLM NTLM_WB PSL SPNEGO SSL TLS-SRP UnixSockets zstd

/home/schoenberg/work/study/lean/mathematics_in_lean> git --version
git version 2.34.1

> elan toolchain install leanprover/lean4:v4.30.0
warning: could not check for elan self-update: error during download
info: downloading https://releases.lean-lang.org/lean4/v4.30.0/lean-4.30.0-linux.tar.zst
error: could not download file from 'https://releases.lean-lang.org/lean4/v4.30.0/lean-4.30.0-linux.tar.zst' to '/opt/elan/tmp/k_4b23rp_oa1f5f__file'
info: caused by: error during download
info: caused by: [60] SSL peer certificate or SSH remote key was not OK
=> Operation failed. Exit code: 1.

It is failed due to my bad network.

However, I have installed elan and lean on my PC already, why it comes out to download and install again?

[mhuisi]

What does elan dump-state yield in /home/schoenberg/work/study/lean/mathematics_in_lean?

[wieniawski-lai]

What does elan dump-state yield in /home/schoenberg/work/study/lean/mathematics_in_lean?

what do you mean by elan dump-state?

elan, lake and other excuting file in bin?
toolchains?

You mean I need a copy of total bin and toolchains under workding directory?

[mhuisi]

what do you mean by elan dump-state?

Elan is Lean's version manager. It is what is trying to install the toolchain in the output you posted earlier.
Running the command elan dump-state from the terminal in your project folder tells me what state Elan is in.

You mean I need a copy of total bin and toolchains under workding directory?

Your installation of Elan needs to be complete, yes.

[wieniawski-lai]

My LEAN_HOME=/opt/elan
My working directory is under /home/schoenberg/work/study/lean/mathematics_in_lean, which equals to /mnt/hdd0/work/study/lean/mathematics_in_lean.
I have copied bin, toolchains, env, known-projects and settings.toml from ELAN_HOME to my working directory.
Then I typed elan dump-state, it returns:

{
  "elan_version": {
    "current": "4.2.3",
    "newest": {
      "Ok": "4.2.3"
    }
  },
  "toolchains": {
    "installed": [
      {
        "resolved_name": "lean-4.30.0-linux",
        "path": "/opt/elan/toolchains/lean-4.30.0-linux"
      },
      {
        "resolved_name": "lean-4.33.0-linux",
        "path": "/opt/elan/toolchains/lean-4.33.0-linux"
      }
    ],
    "default": {
      "unresolved": {
        "Remote": {
          "origin": "leanprover/lean4",
          "release": "stable",
          "from_channel": "stable"
        }
      },
      "resolved": {
        "live": {
          "Ok": "leanprover/lean4:v4.33.0"
        },
        "cached": null
      }
    },
    "active_override": {
      "unresolved": {
        "Remote": {
          "origin": "leanprover/lean4",
          "release": "v4.30.0",
          "from_channel": null
        }
      },
      "reason": {
        "ToolchainFile": "/mnt/hdd0/work/study/lean/mathematics_in_lean/lean-toolchain"
      }
    },
    "resolved_active": {
      "live": {
        "Ok": "leanprover/lean4:v4.30.0"
      },
      "cached": "leanprover/lean4:v4.30.0"
    }
  }
}

But we I start VSCode, it still trying to download lean4:v4.30.0

> elan toolchain install leanprover/lean4:v4.30.0
info: downloading https://releases.lean-lang.org/lean4/v4.30.0/lean-4.30.0-linux.tar.zst

Any idea?

[mhuisi]

Ah, I see. The problem is that the toolchains you manually installed under toolchains are not named correctly. On your machine, they are called lean-4.30.0-linux and lean-4.33.0-linux, but the correct names are leanprover--lean4---v4.30.0 and leanprover--lean4---v4.33.0.

I'd try the following:

cd /opt/elan/toolchains
mv lean-4.30.0-linux leanprover--lean4---v4.30.0
mv lean-4.33.0-linux leanprover--lean4---v4.33.0

(BTW, you do not actually need Elan in your working directory. I misunderstood your earlier question as whether your installation of Elan needs all of these folders.)

[wieniawski-lai]

Ah, I see. The problem is that the toolchains you manually installed under toolchains are not named correctly. On your machine, they are called lean-4.30.0-linux and lean-4.33.0-linux, but the correct names are leanprover--lean4---v4.30.0 and leanprover--lean4---v4.33.0.

I'd try the following:

cd /opt/elan/toolchains
mv lean-4.30.0-linux leanprover--lean4---v4.30.0
mv lean-4.33.0-linux leanprover--lean4---v4.33.0

Yes, that's correct. Thanks a lot! The VScode doesnot go on downloading toolchain again.
Thanks!
That really helps.

(BTW, you do not actually need Elan in your _working directory_. I misunderstood your earlier question as whether your installation of Elan needs all of these folders.)

However, when I open VSCode again, it begins go clone mathlib into /.lake/packages/mathlib. (where =mathematics_in_lean root directory)

You know, I stuck again due to my bad network.

info: mathlib: cloning https://github.com/leanprover-community/mathlib4
info: stderr:
Cloning into '/mnt/hdd0/work/study/lean/mathematics_in_lean/.lake/packages/mathlib'...
fatal: unable to access 'https://github.com/leanprover-community/mathlib4/': Failed to connect to github.com port 443 after 136442 ms: Couldn't connect to server
error: external command 'git' exited with code 128

Futurenatelly, I cloned mathlib repo on another PC, and copied to by current PC.

cp <mathlib-repo> <MIL>/.lake/packages/mathlib

And my folder hierachy under <MIL>/.lake/packages/ is

However, when I start VSCode again, it removes all the files under /.lake/pachages/mathlib and starts to clone mathlib4 from github.

Here is my question:

1. mathlib4 is a package needed by MIL. It should be installed under ./lake/pakcages. I only copied the cloned repo there. Do I need to register it to my enviroment to let LEAN to find it? like to update some tmol file to specify the directory of it?
2. What I copied is the repo itself. Do I need to compile it?
3. I guess it likes nodejs npm, the packages are downaloded and install under working directory, which is locally. Is there a way to install the package globally, like in /opt/lean/pakcages, so that every project can use the same package, instead to install it again and again locally?

thx

[mhuisi]

Does the version of Mathlib that you copied into .lake/packages have the right Git revision that is pinned by MIL?
On the current master of MiL, this is: https://github.com/leanprover-community/mathematics_in_lean/blob/dd6d752fedb14082f557913c2dccb2d4851e5173/lake-manifest.json#L8

Also note that MiL has more dependencies than just Mathlib.

I'd probably recommend cloning and building MiL on your other machine in its entirety and then copying that over instead of trying to reconstruct the .lake of MiL.

[wieniawski-lai]

Does the version of Mathlib that you copied into .lake/packages have the right Git revision that is pinned by MIL? On the current master of MiL, this is: https://github.com/leanprover-community/mathematics_in_lean/blob/dd6d752fedb14082f557913c2dccb2d4851e5173/lake-manifest.json#L8

Also note that MiL has more dependencies than just Mathlib.

I'd probably recommend cloning and building MiL on your other machine in its entirety and then copying that over instead of trying to reconstruct the .lake of MiL.

thx

I tried as your suggestion which cloning and building MiL then copy entirety.

which solves my problem.

However, the mathlib is installed locally under <MIL>/.lake/packages

Is there a way to install it globally, like under /opt/elan/packages, then other project can use it.

thx

[mhuisi]

There is currently no easy and battle-tested way to do this, though we are actively working on a new local caching mechanism that does this automatically and shares build artifacts between projects on your machine.