Lean compilation process

Stream: new members

[Giorgio Mossa]

Hello everyone, new member here and most importantly new to Lean. I would like to understand how does the lean and lake commands process lean files. Is there any reference, such as man pages that explains things like "how these two commands work", "which environment variables they use", etc? Thank you in advance for any answer.

[Julian Berman]

Welcome!
When you say "how do the commands work" -- do you mean end-user explanations of how you use the commands? Or do you really mean "how do they work internally"?

[Giorgio Mossa]

Julian Berman ha scritto:

Welcome!
When you say "how do the commands work" -- do you mean end-user explanations of how you use the commands? Or do you really mean "how do they work internally"?

Well...I'd like an answer to both questions.

[Julian Berman]

As far as I know, neither ship with a man page (yet, hopefully). Lake's user documentation is in its README: https://github.com/leanprover/lake. Running the lean binary directly is fairly uncommon, since the vast majority of users use it via elan, though that essentially just gives you something with the same user-facing interface. As far as I know the most CLI-specific documentation that exists is in lean --help.

[Julian Berman]

I'm not sure what specifically you're looking for internally, but there's e.g. the developing Lean documentation: https://lean-lang.org/lean4/doc/dev/index.html and there's a #lean4 dev stream where you can likely ask specific questions

[Julian Berman]

Of course if you're looking for how to use or learn Lean the language rather than simply the CLI tool, there's definitely plenty of documentation for that.

[Giorgio Mossa]

First of all thanks for your answers. Basically, I believe that more I understand a system as a whole the better I can use it.
In the short term I would like to understand how the import-system work, in particular I am having trouble importing modules from different projects I have created.

[Giorgio Mossa]

On the long run I would also like to write down programs in Lean and later on to port them to different architectures: by compiling the lean code to C-files and later compiling said C-file in the foreign architecture.

[Giorgio Mossa]

To achieve this, it seems to me that I would need to understand the compilation process.

[Julian Berman]

For importing from multiple projects you probably want to look at the lake documentation for declaring dependencies -- https://github.com/leanprover/lake#syntax-of-require

[Giorgio Mossa]

Indeed this seems to be the solution. Thank you again.