## Stream: general

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

#### 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'}


#### 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

#### 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?

#### 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

#### Daniel Donnelly (Dec 05 2019 at 03:18):

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

#### 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

#### Mario Carneiro (Dec 05 2019 at 03:18):

make sure that lean test.lean works

#### Mario Carneiro (Dec 05 2019 at 03:18):

without using the server mode

#### Mario Carneiro (Dec 05 2019 at 03:19):

Oh and clear the LEAN_PATH env variable

#### Mario Carneiro (Dec 05 2019 at 03:19):

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

#### Mario Carneiro (Dec 05 2019 at 03:19):

we really need to fix the error message

#### 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

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

#### Mario Carneiro (Dec 05 2019 at 03:24):

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

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

#### 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!

#### 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

#### 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

#### Mario Carneiro (Dec 05 2019 at 03:27):

and it will save .olean files for the core library

#### Mario Carneiro (Dec 05 2019 at 03:27):

after that, checking simple things should be fast

#### 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