Zulip Chat Archive

Stream: new members

Topic: linux binary installation

view this post on Zulip Manoj Kummini (Sep 26 2020 at 05:53):

I have two standalone linux binary installations 3.4.2 and 3.9.0 (nightly-2020-04-28), and I choose between these two by changing PATH in .bashrc. I have also installed mathlib (globally) running leanproject global-install in two different directories under ~/. (I made ~/.lean a symbolic link, pointing to the correct mathlib directory, depending on which version of the binary I have in my PATH. With the 3.4.2 binary and the corresponding mathlib, things are OK, except for that it is older. (E.g., analysis/special_functions is not in the mathlib corresponding to 3.4.2.) However, 3.9.0 with its mathlib hangs, even on a simple input file with two lines

import data.real.basic
#check real

(top shows lean using 600-700% CPU and 15-20% memory.) Using the newer mathlib with 3.4.2 binary throws up a lot of errors, the first of which is

..../_target/deps/mathlib/src/control/basic.lean:89:1: error: type mismatch at application
  bind_map_eq_seq f

I wonder if anyone has come across similar problems, and have any work-around.

view this post on Zulip Scott Morrison (Sep 26 2020 at 06:06):

I think the work-around is to not attempt to manage Lean versions by hand, but instead follow the installation instructions and use elan to automatically select the Lean version, then specify the lean version you want on a per-project basis in your leanpkg.toml file.

view this post on Zulip Scott Morrison (Sep 26 2020 at 06:07):

I would strongly recommend throwing out whatever you created with global-install, and similarly throwing out an symbolic links you've made for ~/.lean. Doing anything like this is inviting disaster, and makes it impossible for us to help.

Last updated: May 16 2021 at 05:21 UTC