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

Stream: general

[Daniel Donnelly]

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]

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]

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]

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

[Daniel Donnelly]

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

[Mario Carneiro]

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]

make sure that lean test.lean works

[Mario Carneiro]

without using the server mode

[Mario Carneiro]

Oh and clear the LEAN_PATH env variable

[Mario Carneiro]

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

[Mario Carneiro]

we really need to fix the error message

[Mario Carneiro]

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]

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]

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

[Daniel Donnelly]

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]

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]

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]

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]

and it will save .olean files for the core library

[Mario Carneiro]

after that, checking simple things should be fast

[Daniel Donnelly]

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.