Lpo files contain absolute positions #1436

Activity

1. sacerdot commented on Jul 2, 2026

   

   sacerdot

   on Jul 2, 2026

   Collaborator

   More actions

   I confirm the bug, but sig_state_of_require is not the culprit. The culprit is due to the usage in the LSP of a "local" file that is actually installed using lambdapi install that relocates the file. The .lpo were not thought to be relocatable when implementing search (and indeed they are not): they concaint positions with absolute paths. The exception is raised when trying to access a file that has been moved. In particular this is required: 1) to synthesize a QID for rule names that have none ; 2) to show the query results
2. fblanqui

   changed the title [-]New require open breaks LSP server[/-] [+]Lpo files contain absolute positions[/+] on Jul 10, 2026
3. fblanqui commented on Jul 10, 2026

   

   fblanqui

   on Jul 10, 2026

   Member

   More actions

   The complete error message in VSCode is:

   file:///home/blanqui/src/lambdapi/tests/OK/apply.lp:1:0-23/home/blanqui/.opam/5.5.0/.opam-switch/build/lambdapi-stdlib.1.4.0/Prop.lp cannot be mapped under the library root.
   Consider adding a package file under your source tree, or use the [--map-dir] option.
   

   In Emacs, I get:

   Syntax error. Expected: "open", "private", "qualified identifier".
   

   Strange...
4. fblanqui commented on Jul 10, 2026

   

   fblanqui

   on Jul 10, 2026

   Member

   More actions

   Concerning lpo files, what about using relative positions? The absolute position could be obtained on the fly by using file_of_path?
5. fblanqui commented on Jul 10, 2026

   

   fblanqui

   on Jul 10, 2026

   Member

   More actions

   With #1455, I get in VSCode:

   /home/blanqui/.LPSearch.db: No such file or directory.
   Type "lambdapi index --help" to learn how to create the index.
   file:///home/blanqui/src/lambdapi/tests/OK/apply.lp:1:0-23"/home/blanqui/.opam/5.5.0/.opam-switch/build/lambdapi-stdlib.1.4.0/Prop.lp" cannot be mapped under the library root.
   Consider adding a package file under your source tree, or use the [--map-dir] option.
   

   Note that there is no space or newline between the position and the error message.
6. fblanqui

   added a commit that references this issue on Jul 10, 2026

   Do not fail in case of moved file (#1439)

   ...

   1ac2f3c