Installation issues

Stream: general

[Stefan Sterea]

I created this topic because it seems like there is no topic to talk about issues regarding getting started

[Stefan Sterea]

I want to start this topic by asking for help: I've installed lean binaries and set the extension path in VS Code to the lean executable. I followed the instructon to install mathlibtools via pip and now I'm stuck. When I want to create a project and write leanproject new my_project in Git Bash it gives the error [WinError 2] The system cannot find the file specified.

[Stefan Sterea]

When I do leanproject --debug new I get this stack trace:

  File "c:\users\hp\appdata\local\programs\python\python39\lib\runpy.py", line 197, in _run_module_as_main
    return _run_code(code, main_globals, None,
  File "c:\users\hp\appdata\local\programs\python\python39\lib\runpy.py", line 87, in _run_code
    exec(code, run_globals)
  File "C:\Users\HP\AppData\Local\Programs\Python\Python39\Scripts\leanproject.exe\__main__.py", line 7, in <module>
  File "c:\users\hp\appdata\local\programs\python\python39\lib\site-packages\mathlibtools\leanproject.py", line 359, in safe_cli
    handle_exception(err, str(err))
  File "c:\users\hp\appdata\local\programs\python\python39\lib\site-packages\mathlibtools\leanproject.py", line 63, in handle_exception
    raise exc
  File "c:\users\hp\appdata\local\programs\python\python39\lib\site-packages\mathlibtools\leanproject.py", line 357, in safe_cli
    cli() # pylint: disable=no-value-for-parameter
  File "c:\users\hp\appdata\local\programs\python\python39\lib\site-packages\click\core.py", line 829, in __call__
    return self.main(*args, **kwargs)
  File "c:\users\hp\appdata\local\programs\python\python39\lib\site-packages\click\core.py", line 782, in main
    rv = self.invoke(ctx)
  File "c:\users\hp\appdata\local\programs\python\python39\lib\site-packages\click\core.py", line 1259, in invoke
    return _process_result(sub_ctx.command.invoke(sub_ctx))
  File "c:\users\hp\appdata\local\programs\python\python39\lib\site-packages\click\core.py", line 1066, in invoke
    return ctx.invoke(self.callback, **ctx.params)
  File "c:\users\hp\appdata\local\programs\python\python39\lib\site-packages\click\core.py", line 610, in invoke
    return callback(*args, **kwargs)
  File "c:\users\hp\appdata\local\programs\python\python39\lib\site-packages\mathlibtools\leanproject.py", line 94, in new
    LeanProject.new(Path(path), cache_url, force_download)
  File "c:\users\hp\appdata\local\programs\python\python39\lib\site-packages\mathlibtools\lib.py", line 526, in new
    subprocess.run(['leanpkg', 'init', path.absolute().name], check=True)
  File "c:\users\hp\appdata\local\programs\python\python39\lib\subprocess.py", line 505, in run
    with Popen(*popenargs, **kwargs) as process:
  File "c:\users\hp\appdata\local\programs\python\python39\lib\subprocess.py", line 951, in __init__
    self._execute_child(args, executable, preexec_fn, close_fds,
  File "c:\users\hp\appdata\local\programs\python\python39\lib\subprocess.py", line 1420, in _execute_child
    hp, ht, pid, tid = _winapi.CreateProcess(executable, args,
FileNotFoundError: [WinError 2] The system cannot find the file specified```

[Kevin Buzzard]

I don't know what you're reading but if you're setting the extension path in VS Code then you're already doing something very wrong. I would unset that right now. Where are you reading this? The canonical installation instructions for Lean 3 are here, and Lean 4 is not recommended for beginners as it's still in alpha and there's not much documentation.

[Kevin Buzzard]

You're also not supposed to be installing Lean binaries directly, at least if you're using Lean 3. Perhaps you can clarify whether you're trying to install Lean 3 or Lean 4, and if you're not sure then perhaps you want to explain what you want to do with Lean so we can suggest which one to go with. By default we suggest new users install Lean 3.

[Stefan Sterea]

I'm using Lean 3. I set the extension path to the lean executable because I didn't want to install elan, I didn't think it would be necessary since I had already downloaded the binaries and it works. The only thing that doesn't work is the leanproject command

[Kevin Buzzard]

I believe leanproject uses elan under the hood so I suspect that if you don't use elan you can't have leanproject.

[Kevin Buzzard]

It goes without saying that of course I'd recommend the standard installation procedure, this chat is littered with the remains of people who tried to do it their own way and ran into problems. But of course it's up to you. Do you also want to use mathlib? If you do then I really would recommend leanproject. If you don't (e.g. you're not doing maths and you don't need access to any of the mathlib tactics and can make do with the core Lean 3 tactics) then you can probably get away with installing a binary. Are you installing 3.4.2 (which has some buggy tactics) or 3.26.whatever (whatever the community version is nowadays)?

[Yakov Pechersky]

A reason to have elan: when working with newer or older branches of mathlib, leanproject will automatically install the proper lean toolchain via elan, since each mathlib commit is really only valid for one lean release.

[Kevin Buzzard]

The only reason to not have it is if you are convinced that you will never need any of the things in mathlib and are equally convinced that you are never going to want to upgrade your lean version, and furthermore you are happy to compile lean yourself rather than take advantage of the free binaries for your OS which elan provides. For me this is a narrow-minded approach but we've seen people before who are edgy about installing any more software than they absolutely need at this point in time. I can understand that some people might prefer this approach in general but as I've already said, it's not hard to find cases where people have just got stuck when trying this with lean for all manner of reasons and individual cases are hard to debug. Of course it is still possible to get working, presumably people were doing this before elan, but I showed up in 2017 and elan was already there so I used it

[Stefan Sterea]

Thanks. I do need mathlib and now I understand I have to install elan. I was just being picky about what I need and what I don't in order to save memory but now I see that it's a necessity.

[Yakov Pechersky]

elan does not run in the background. Think of it more like a package manager