Zulip Chat Archive
Stream: general
Topic: How do you `update-mathlib`
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.
Patrick Massot (Dec 16 2019 at 20:33):
Where do you see python -m on that page?
Daniel Donnelly (Dec 16 2019 at 20:35):
Where do you see
python -mon that page?
I'm saying I also tried that :D
Patrick Massot (Dec 16 2019 at 20:36):
I see.
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".
Daniel Donnelly (Dec 16 2019 at 20:39):
B
Patrick Massot (Dec 16 2019 at 20:42):
https://leanprover-community.github.io/lean-web-editor/
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?
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?
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".
Daniel Donnelly (Dec 16 2019 at 21:10):
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.
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.
Patrick Massot (Dec 16 2019 at 21:13):
Can't you package Lean with your stuff?
Patrick Massot (Dec 16 2019 at 21:13):
You won't need to update mathlib without updating your thing, right?
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.
Patrick Massot (Dec 16 2019 at 21:16):
But you'll somehow expect users to be able to run python code, right?
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 .
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.
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.
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.
Patrick Massot (Dec 16 2019 at 21:24):
Lean doesn't require python. It's only community developed supporting tools that use it.
Patrick Massot (Dec 16 2019 at 21:24):
Why don't you read the source code of update-mathlib since you can read python?
Daniel Donnelly (Dec 16 2019 at 21:25):
@Patrick Massot yes, good idea!
Daniel Donnelly (Dec 16 2019 at 21:26):
Sometimes it takes another perspective to solve a problem :D
Last updated: Dec 20 2023 at 11:08 UTC