Zulip Chat Archive

Stream: new members

Topic: no leanpkg.exe

Lewis (Oct 27 2023 at 12:16):

Hello, why does the installed bin directory under .elan\toolchains\leanprover--lean4---stable contain no leanpkg.exe? and without it, how to install Mathlib4? Thanks a lot!

Lewis (Oct 27 2023 at 12:17):

Hello, why does the installed bin directory under .elan\toolchains\leanprover--lean4---stable contain no leanpkg.exe? and without it, how to install Mathlib4? Thanks a lot!

Notification Bot (Oct 27 2023 at 12:18):

A message was moved here from #maths > left vs right modules in tensor products by Eric Wieser.

Eric Wieser (Oct 27 2023 at 12:19):

@Lewis, Why are you expecting a leanpkg.exe? Can you link to the instructions you are following?

Notification Bot (Oct 27 2023 at 12:19):

A message was moved here from #mathlib4 > std4#183, lemmas about Bool by Eric Wieser.

Lewis (Oct 27 2023 at 12:22):

Hello, why does the installed bin directory under .elan\toolchains\leanprover--lean4---stable contain no leanpkg.exe? and without it, how to install Mathlib4? Thanks a lot!

Mauricio Collares (Oct 27 2023 at 12:34):

leanpkg is Lean 3. Can you tell us which instructions you're currently following? This will help the maintainers fix the instructions for future users.

Notification Bot (Oct 27 2023 at 13:43):

2 messages were moved here from #lean4 > No leanpkg.exe? by Eric Wieser.

Eric Wieser (Oct 27 2023 at 13:45):

@Lewis, it seems you might be struggling with Zulip; please search for your previous posts rather than repeatedly posting the same question. Zulip is not like IRC where the only way to get your message seen is to repost it!

Mario Carneiro (Oct 27 2023 at 13:45):

Please don't cross-post messages. If you must, use links to a single canonical place instead of re-posting the same text in multiple places

Patrick Massot (Oct 27 2023 at 13:47):

And don't post messages in random existing conversations.

Lewis (Oct 28 2023 at 01:00):

Eric Wieser said:

Lewis, Why are you expecting a leanpkg.exe? Can you link to the instructions you are following?

I was following the error message in termal; Without leanpkg.exe, how to install mathlib4? Thanks

Mauricio Collares (Oct 28 2023 at 01:04):

But did you read about leanpkg somewhere? The most up-to-date instructions for getting started are at https://leanprover-community.github.io/get_started.html, but it would be really useful if you could point out where leanpkg is being mentioned so the instructions can be updated.

Mauricio Collares (Oct 28 2023 at 01:07):

You don't install mathlib system-wide. Instead, you git clone projects that depend on mathlib (or git clone mathlob itself), or start your own project using mathlib. You can read more about it at https://leanprover-community.github.io/install/project.html.

Last updated: Dec 20 2023 at 11:08 UTC