Zulip Chat Archive

Stream: general

Topic: Error creating new project

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

    leanpkg configure
to get leanpkg ready

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

    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).

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

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:

Daniel Donnelly (Aug 28 2019 at 20:27):

pasted image

Daniel Donnelly (Aug 28 2019 at 20:27):

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

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)

Daniel Donnelly (Aug 28 2019 at 20:31):

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

Daniel Donnelly (Aug 28 2019 at 20:35):

It's working now :D

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: Aug 03 2023 at 10:10 UTC