linux binary installation

Stream: new members

[Manoj Kummini]

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.

[Scott Morrison]

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.

[Scott Morrison]

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.