search

leanprover / LeanInk

LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
Apache License 2.0
60 stars 16 forks source link

Load LeanSearchPaths #9

Closed insightmind closed 2 years ago

insightmind commented 3 years ago

Description

To execute a lean file, we need to load the local search paths to get access to Lean module, most importantly the Init module.

Detailed behaviour

We can either manually search through the system to find the Lean search paths or use a similar approach to either Lake or LeanServer.

However getting the searchPaths for Lean is only a part of the problem that needs to be solved. Another problem resides in third party dependencies and on disk file dependencies. Because in the current solution, the Lean4 Alectryon driver generates a new local temporary Lean file and calls LeanInk on that file. However if this file contains references, e.g.: 3rd party lake dependencies, like mathlib, or another file in the same project, these dependencies won't be propagated over to LeanInk. We have to find a good solution to support this case, so we can make sure the dependencies are available on analysis.

Testscenarios

References

Kha commented 2 years ago

If lean is in the PATH, we can use Lake.findLeanInstall? to locate at least the stdlib and tell Lean about it. For external dependencies, we should assume that they are handled by a lakefile.lean, in which case we can ask Lake to produce the search path for them: https://github.com/leanprover/lean4/blob/3546104959f6048adfcbde5e72a1ca98abf03e6f/src/Lean/Server/FileWorker.lean#L120-L123

insightmind commented 2 years ago

Referencing: https://github.com/leanprover/lean4/pull/805

tydeu commented 2 years ago

I recently put on my lake TODO list a lake env command (feel free to suggest a better name!) which would execute a given shell command with the environment properly set (e.g., lake env lean <args> would execute lean with a LEAN_PATH including the projects dependencies). That may help here. That is, you could use lake env lean-ink .. and the search path would be setup as desired. I should be able to prioritize that and get it done this weekend (it is a rather trivial addition) if it would be useful.

insightmind commented 2 years ago

The workaround with using lake as a dependency works fine for now :-) so no rush there. Eventually it's probably a good idea to add this tho.