Zulip Chat Archive

Stream: general

Topic: What is 'init' and how do I create it?


view this post on Zulip Daniel Donnelly (Dec 05 2019 at 03:05):

I'm connecting to Lean with python code. Here's the first server response after synching on an existing file (so yes it's finding test.lean), but not this init requirement:

Lean =>:
{'msgs': [{'caption': '',
           'file_name': 'test.lean',
           'pos_col': 0,
           'pos_line': 1,
           'severity': 'error',
           'text': "file 'init' not found in the LEAN_PATH"}],
 'response': 'all_messages'}

view this post on Zulip Mario Carneiro (Dec 05 2019 at 03:11):

init is a folder in the lean repo; it should be at library/init relative to the repo root. Any lean file that does not begin with prelude implicitly starts with import init which loads the file library/init/default.lean. Lean finds this file by navigating from the lean.exe executable location, so if you copy lean.exe out of its directory you get this error

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

init is a folder in the lean repo; it should be at library/init relative to the repo root. Any lean file that does not begin with prelude implicitly starts with import init which loads the file library/init/default.lean. Lean finds this file by navigating from the lean.exe executable location, so if you copy lean.exe out of its directory you get this error

I have not done that. I have copied the entire lean folder into a subfolder lean. Inside is bin containing lean.exe. The current working directory that lean is using though is . So lean is contained in ./lean/bin/lean.exe and its using . as to where to find test.lean that I am syncing. Is there some instructions on setting up a default lean workspace?

view this post on Zulip Mario Carneiro (Dec 05 2019 at 03:17):

As far as I can tell from the code, lean does not use the pwd at all for finding the builtin_path

view this post on Zulip Daniel Donnelly (Dec 05 2019 at 03:18):

my LEAN_PATH = lean relative to . could this be why?

view this post on Zulip Mario Carneiro (Dec 05 2019 at 03:18):

it uses various tricks on win/OSX/linux to find where the executable itself is and navigates from that, so if lean/library/init/default.lean is there then it should work

view this post on Zulip Mario Carneiro (Dec 05 2019 at 03:18):

make sure that lean test.lean works

view this post on Zulip Mario Carneiro (Dec 05 2019 at 03:18):

without using the server mode

view this post on Zulip Mario Carneiro (Dec 05 2019 at 03:19):

Oh and clear the LEAN_PATH env variable

view this post on Zulip Mario Carneiro (Dec 05 2019 at 03:19):

don't ever set it, that's from an old version of lean

view this post on Zulip Mario Carneiro (Dec 05 2019 at 03:19):

we really need to fix the error message

view this post on Zulip Mario Carneiro (Dec 05 2019 at 03:20):

the "modern" way to set the lean path is to have a leanpkg.path file in some parent of the target lean file, usually created by the leanpkg tool

view this post on Zulip Daniel Donnelly (Dec 05 2019 at 03:23):

the "modern" way to set the lean path is to have a leanpkg.path file in some parent of the target lean file, usually created by the leanpkg tool

lean.exe test.lean runs and does nothing so I assume it's working. I've just put a #check 1 in it.

view this post on Zulip Mario Carneiro (Dec 05 2019 at 03:24):

I would expect it to print something with that check line though

view this post on Zulip Daniel Donnelly (Dec 05 2019 at 03:25):

I would expect it to print something with that check line though

How do I get leanpkg to work what do I pass it? It just sits and does nothing when run without args.

view this post on Zulip Daniel Donnelly (Dec 05 2019 at 03:25):

I would expect it to print something with that check line though

How do I get leanpkg to work what do I pass it? It just sits and does nothing when run without args.

Nevermind, it finally returned with help!

view this post on Zulip Mario Carneiro (Dec 05 2019 at 03:26):

Is there some instructions on setting up a default lean workspace?

There is a tutorial project on the mathlib website: https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md#working-on-an-existing-package

view this post on Zulip Mario Carneiro (Dec 05 2019 at 03:26):

When it takes forever to return like that, it probably means that the library is not compiled. Run lean --make test.lean instead

view this post on Zulip Mario Carneiro (Dec 05 2019 at 03:27):

and it will save .olean files for the core library

view this post on Zulip Mario Carneiro (Dec 05 2019 at 03:27):

after that, checking simple things should be fast

view this post on Zulip Daniel Donnelly (Dec 05 2019 at 03:31):

Is there some instructions on setting up a default lean workspace?

There is a tutorial project on the mathlib website: https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md#working-on-an-existing-package

Thanks @Mario Carneiro that's just what I needed.


Last updated: May 11 2021 at 00:31 UTC