Zulip Chat Archive

Stream: general

Topic: Error creating new project


view this post on Zulip Daniel Donnelly (Aug 28 2019 at 20:04):

My goal is to import stuff from mathlib.

pasted image
That's the step that I get to according to the instructions:

Working on an existing package

If you have not logged in type
    source ~/.profile.

Clone the repo of the project you want to get

Cd to the project folder

Type
    leanpkg configure
to get leanpkg ready

python $HOME/.mathlib/bin/update-mathlib

Type
    leanpkg build
to compile everything, this will take some time.

launch VScode, either through your application menu or by typing code

On the main screen, or in the File menu, click "Open folder"

Choose the folder lean-perfectoid-spaces (not one of its subfolders).

view this post on Zulip Simon Hudon (Aug 28 2019 at 20:24):

The long number it gives you is a commit of mathlib. On github, go to that commit to make sure that it exists

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 20:27):

I'm creating it from scratch. Now intellisense shows that algebra.CommRing is there (in dropsown) but it results in import error still:

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 20:27):

pasted image

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 20:27):

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

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 20:30):

Now there's no error red zigzag line, however, it's taking a long time to update Messages (hasn't updated even yet)

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 20:31):

Lean is working now, it's just updating in the bg (?)

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 20:35):

It's working now :D

view this post on Zulip Daniel Donnelly (Aug 28 2019 at 20:36):

import algebra.all

I also needed to run the mk_all.sh script from where it is placed by leanpkg


Last updated: May 13 2021 at 04:21 UTC