Zulip Chat Archive

Stream: general

Topic: How do you `update-mathlib`


view this post on Zulip Daniel Donnelly (Dec 16 2019 at 20:28):

The instructions here:
https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md

Don't work completely on Windows 10 / VSCode. They work up to and not including update-mathlib. Tried:

python -m update-mathlib

Not found.

Nothing is highlighted in my test.lean file, and there is no Lean Messages display.

view this post on Zulip Patrick Massot (Dec 16 2019 at 20:33):

Where do you see python -m on that page?

view this post on Zulip Daniel Donnelly (Dec 16 2019 at 20:35):

Where do you see python -m on that page?

I'm saying I also tried that :D

view this post on Zulip Patrick Massot (Dec 16 2019 at 20:36):

I see.

view this post on Zulip Daniel Donnelly (Dec 16 2019 at 20:37):

@Patrick Massot Another quick question, how do you get to the online debug version of : https://leanprover.github.io/live/latest/

I need it to study its messages for the IDE I'm making for Lean.

The debug version is the one with a question mark "?" drop down with settings on which I select "display log messages".

view this post on Zulip Daniel Donnelly (Dec 16 2019 at 20:39):

B

view this post on Zulip Patrick Massot (Dec 16 2019 at 20:42):

https://leanprover-community.github.io/lean-web-editor/

view this post on Zulip Patrick Massot (Dec 16 2019 at 20:43):

Did you follow https://github.com/leanprover-community/mathlib/blob/master/docs/install/windows.md before the project handling page?

view this post on Zulip Daniel Donnelly (Dec 16 2019 at 20:49):

@Patrick Massot I'm doing that now, but how does my IDE accomplish the same thing or will it definitely need a git-bash installed to use curl?

view this post on Zulip Patrick Massot (Dec 16 2019 at 20:51):

I'm sorry, I don't understand you question. What are "your IDE" and "the same thing".

view this post on Zulip Daniel Donnelly (Dec 16 2019 at 21:10):

suTdvHG6Nj.png

Here's a screenshot. I'm trying to add a visual component to a proof assistant. I gave up on Coq trying to understand the coq_jupyter server code. Now I'm gowing full throttle on Lean. So I'd like setup to be easy, so the user doesn't have to do all of this command line stuff to use Lean.

How do you recommend I install elan without curl. If curl is required, I can just install Git for Windows on windows.

view this post on Zulip Daniel Donnelly (Dec 16 2019 at 21:12):

In the future it could support more than Lean. OTOH the operation of the visual component will depend heavily on the language passed to the proof assistant.

view this post on Zulip Patrick Massot (Dec 16 2019 at 21:13):

Can't you package Lean with your stuff?

view this post on Zulip Patrick Massot (Dec 16 2019 at 21:13):

You won't need to update mathlib without updating your thing, right?

view this post on Zulip Daniel Donnelly (Dec 16 2019 at 21:15):

@Patrick Massot I can only work within the parameters given for regular users. I will have to call various commands yes, but ideally we don't need another install path to maintain, so I just replicate the user install methods.

view this post on Zulip Patrick Massot (Dec 16 2019 at 21:16):

But you'll somehow expect users to be able to run python code, right?

view this post on Zulip Daniel Donnelly (Dec 16 2019 at 21:16):

@Patrick Massot this topic is kind of orthogonal to packaging Lean with my code. Of course I will though! Especially because it can be installed by just unzipping .

view this post on Zulip Daniel Donnelly (Dec 16 2019 at 21:17):

So right now they'll have to install MkTeK and Git for Windows
I will write automators for these install processes.

view this post on Zulip Daniel Donnelly (Dec 16 2019 at 21:18):

@Patrick Massot that is a negative. I use auto-py-to-exe which calls pyinstaller, and that makes a windows exec with all dependencies included. So they don't have to be able to run python to answer you.

view this post on Zulip Daniel Donnelly (Dec 16 2019 at 21:19):

@Patrick Massot But nevermind, because Lean requires it. I just forget because I already have it installed.

view this post on Zulip Patrick Massot (Dec 16 2019 at 21:24):

Lean doesn't require python. It's only community developed supporting tools that use it.

view this post on Zulip Patrick Massot (Dec 16 2019 at 21:24):

Why don't you read the source code of update-mathlib since you can read python?

view this post on Zulip Daniel Donnelly (Dec 16 2019 at 21:25):

@Patrick Massot yes, good idea!

view this post on Zulip Daniel Donnelly (Dec 16 2019 at 21:26):

Sometimes it takes another perspective to solve a problem :D


Last updated: May 14 2021 at 06:16 UTC