File management and module mapping improvement #289
Conversation
|
Thanks @rlepigre for your PR. I don't understand why you need a --lib-root option. It seems to me that the --map option subsumes it. |
|
No, it is not subsumed because it would mean being able to map an "empty" module path, which is not possible. Plus, the library root has a very particular role: every installed library should be installed under it on the system. |
|
It's not clear to me. Please provide an example. |
So, let us assume that we have some library root directory
Globally, this is represented by the following tree: The search for files corresponding to different module paths would then yield:
There are several important things here:
|
|
Why not taking the current directory as the root? I was personally thinking in something different: lambdapi --map r1:d1 .. --map rk:dk file.lp where ri is a non-qualified ident called a root and di is an arbitrary path some roots could also be given through an environment variable $DK_PATH there is also an implicit root r0 mapped to the current directory then in file.lp we can have: require a.b // refers to ./a/b.lp |
|
The root is an actual root: it is the entry point of the module system. So it does not make sense to have the current directory be the root since installed libraries are not installed under the current directory. Of course, the current directory is special, and it should be mapped under a module path that is chosen for the project (maybe automatically by looking at the name of the current directory name, or using a meta data file). I insist that what I proposed here is still work in progress, so everything is not optimal for usability yet. What you propose could maybe work, but I don't see that as a standard approach. (I did not really think your proposal through as much as I did mine, so it's hard for me to understand its limitations.) With what I propose, we will be prepared for having proper tooling (in the line of what Rust has with Cargo), and it also accounts for installation of libraries. Moreover, I don't really like adding yet another syntactic element (your roots). These are not useful since they can just be represented using a normal module path. The location of the corresponding files alone can tell whether a module path corresponds to a library or the a local module. |
|
Why do you want to map module paths to directories and not just roots? |
|
How to handle manually installed libraries with your system, that is, not installed through a system like opam? |
I don't understand that question: what you call "roots" are directories right?
What do you mean by "locally installed libraries"? |
|
In a previous example, you proposed to map foo.bar to some directory. Why would you like to map foo.bar and not just foo? |
|
By locally installed, I mean "manually" installed, that is, not installed using a system like opam. |
Oh, I see. The reason is simple: we may want to have a more complex structure in our libraries that just a flat one. For example, we may want to have the following structure in our installed libraries:
It just gives more options for placing things in relevant directories, and they don't have to be provided by the same package.
Ideally, it should be impossible to install a library "manually", otherwise you get the same mess as with OCaml. But in any case, the approach I propose enforces that libraries are installed under the system's library root. And there is no difference whether they are installed "manually" or automatically. It is just a convention that everyone must respect. |
|
Do you have an example of use of mapping std to dir1 and std.list to a directory that is not a sub-directory of dir1 (even transitively)? |
For |
|
Isn't it a problem to enforce the use of a system like opam? What if the user wants to experiment with some libraries he modified and compiled somewhere in its home directory, for instance, in some git repos? |
Well, that's what the In any case, enforcing the use of a proper tool (nothing like opam, which is crap) is great. It makes everything simpler and more uniform, and the user does not have to care about completely useless details. And also, everything is predictable. |
|
The update of doc/ is missing. |
rlepigre
force-pushed
the
filepath
branch
3 times, most recently
from
abbab7c to
2627025
Compare
|
Hi. Emacs doesn't seem to work with this PR. It would be good to check vscode as well. |
It is supposed to work, @gabrielhdt tried it. Did you reinstall the Emacs mode? For vscode I have no idea how to make the necessary adaptation. There is no documentation and I don't want to spend my time on that, especially since I do not use vscode. |
It seems that pretty much every dedukti/lambdapi's users use emacs in one form or another (evil, dooms, spacemacs, vanilla, ...). I havn't use vscode for months (since I saw the lack of interest of the coq people for vscoq)
|
|
I tested back the emacs mode, with a minimal configuration, and it seems that the proof mode does not work. The rest does. To see it yourself, wget https://sanemacs.com/sanemacs.el
echo '(use-package eglot)' >> sanemacs.el
emacs -q --no-site-file -l sanemacs.el -l <path/to/lambdapi.el>and edit for instance |
|
I can now run emacs (I didn't install LP properly) but it doesn't print whether some thing is well type-checked or not. |
|
No, my fault. lambdapi.pkg is now mandatory even for a single file... Why not but, then, the error message is not very clear: Why not saying that there is no lambdapi.pkg file? Do you test this btw? |
Yes, the I have given some thoughts as to what we could do to make things simpler, but there is no easy solution. Indeed, the error message is not great, I'll improve it. |
|
It's not just when you use the LSP server. It's all the time, even for checking a single file with no dependencies. It's not very convenient. Couldn't we use a default mapping in this case? |
I don't know, I don't have time to take care of that right now. Open an issue about that once this PR is merged and I'll try and find a way. However, I don't think this is going to be a big problem since the only thing you would need is to put a |
PR Deducteam#289 silently removed important unit tests in the Pure module. We try to recover them, but indeed, they don't work, as it seems the library handling API introduced in Deducteam#289 is lacking in terms of how it can be used. There seem to be many problems with the new system in terms of what a language server needs, in particular regarding assumptions about the underlying file system.
The PR #289 broke the vscode plugin. We do a hotfix for now, but the mode still remains broken if using from the dev tree [for example with `dune exec -- code`]. This is quite inconvenient, for now lambdapi must be fully installed as to be used from vscode.
PR Deducteam#289 silently removed important unit tests in the Pure module. We try to recover them, but indeed, they don't work, as it seems the library handling API introduced in Deducteam#289 is lacking in terms of how it can be used. There seem to be many problems with the new system in terms of what a language server needs, in particular regarding assumptions about the underlying file system.
FTR, I wonder on what kind of data this observation is based. Or maybe I misunderstood the claim. |
Hi @maximedenes |
Fixes Deducteam#432 , introduced in Deducteam#289 This whole code needs more investigation as the logic seems quite strange, in particular I think the core of LP should not mess with filesystem low-level details, but hoping for a quick fix.
PR Deducteam#289 silently removed important unit tests in the Pure module. We try to recover them, but indeed, they don't work, as it seems the library handling API introduced in Deducteam#289 is lacking in terms of how it can be used. There seem to be many problems with the new system in terms of what a language server needs, in particular regarding assumptions about the underlying file system.
PR Deducteam#289 silently removed important unit tests in the Pure module. We try to recover them, but indeed, they don't work, as it seems the library handling API introduced in Deducteam#289 is lacking in terms of how it can be used. There seem to be many problems with the new system in terms of what a language server needs, in particular regarding assumptions about the underlying file system.
PR Deducteam#289 silently removed important unit tests in the Pure module. We try to recover them, but indeed, they don't work, as it seems the library handling API introduced in Deducteam#289 is lacking in terms of how it can be used. There seem to be many problems with the new system in terms of what a language server needs, in particular regarding assumptions about the underlying file system.
This PR adresses #243 and several other previous limitations.
Here is the rough idea of the new system (though the work is not finished):
~/.opamdirectory (or some system-wide directory if opam is not used).--lib-rootflag. This is important because the root directory should always be a valid directory, and that is typically not the case prior to installation. So we must now use something likedune exec -- lambdapi check --lib-root libso that thelibdirectory in the source tree is considered the library root. Note that to recover the previous behavior we must run with.as the root.--map-diroption that can be used to map a module path to a specific directory (that may or may not be under the library root). For instance, we might do--map-dir matita:libraries/matitaso that the files under thelibraries/matitafolder correspond to module paths starting withmatitaand then continuing with the underlying directory structure.realpathto get an absolute file name. Note that symbolic links are removed, so we cannot use a symbolic link to include a sub-tree under some mapped module path.Things that remain to be done:
lib/std,libbeing intended as the library root. As a consequence, the modules of the standard library would be accessed withstd.boolfor example (filelib/std/bool.lp). Thelibdirectory should then be installed as the library root of the system.lambdapi lsp --standard-lsp.