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

Commit to mitigate Issue #1436

lambdapi install moves .lp and .lpo files into the standard lib_root; moreover when "lambdapi build" is called from opam, the files are also moved to yet another location (inside the sandbox) to compile them.

However, the .lpo are NOT relocatable in the sense that filenames inside positions `pos` are absolute path. We use them:
a) during indexing of rules to build a `qualid` for the rule
b) to open the file to show the result of queries

Both use cases (a and b) used to fail. In particular, a) prevented to import a library from the standard `lib_root`.

As a mitigation, we replace the hard failures with degradation of functionality. Further work will be necessary to restore the full functionality. In particular, libraries installed in stdlib_root should always be globally indexed.

Author: sacerdot

src/common/pos.ml

@@ -209,8 +209,10 @@ let print_file_contents :
   | Some { fname=Some fname; start_line; start_col; end_line; end_col } ->
      (* WARNING: do not try to understand the following code!
         It's dangerous for your health! *)
-
-     let input_line,finish = parse_file fname in
+    begin match parse_file fname with
+    | exception _ ->
+       string ppf ("Cannot open file \""^fname^"\". Maybe it was moved?")
+    | input_line,finish ->
      let out =
        Buffer.create
         ((end_line - start_line) * 80 +
@@ -273,6 +275,7 @@ let print_file_contents :
 
      finish () ;
      string ppf (Buffer.contents out)
+    end
   | None | Some {fname=None} ->
       if complain_if_location_unknown then
        string ppf (db ^ "unknown location" ^ de)

src/core/sign.ml

@@ -228,11 +228,11 @@ let unlink : t -> unit = fun sign ->
 
 (** [add_symbol_callback] is used to index symbols in the document currently
     edited in Spl mode*)
-let add_symbol_callback = Stdlib.ref (fun _ -> ())
+let add_symbol_callback = Stdlib.ref (fun ~path:_ _ -> ())
 
 (** [add_rules_callback] is used to index rules in the document currently
     edited in Spl mode*)
-let add_rules_callback = Stdlib.ref (fun _ _ -> ())
+let add_rules_callback = Stdlib.ref (fun ~path:_ _ _ -> ())
 
 (** [add_symbol sign expo prop mstrat opaq name pos typ impl notation] adds in
     the signature [sign] a symbol with name [name], exposition [expo],
@@ -248,7 +248,8 @@ let add_symbol : t -> expo -> prop -> match_strat -> bool -> strloc ->
       (cleanup typ) (minimize_impl impl)
   in
   sign.sign_symbols := StrMap.add name.elt sym !(sign.sign_symbols);
-  if Stdlib.(!Common.Console.lsp_mod) then Stdlib.(!add_symbol_callback sym) ;
+  if Stdlib.(!Common.Console.lsp_mod) then
+    Stdlib.(!add_symbol_callback ~path:sign.sign_path sym) ;
   sym
 
 (** [strip_private sign] removes private symbols from signature [sign]. *)
@@ -362,7 +363,8 @@ let add_rules : t -> sym -> rule list -> unit = fun sign s rs ->
     let d = {d with dep_symbols=sm} in
     sign.sign_deps := Path.Map.add s.sym_path d !(sign.sign_deps)
    end ;
-  if Stdlib.(!Common.Console.lsp_mod) then Stdlib.(!add_rules_callback s rs)
+  if Stdlib.(!Common.Console.lsp_mod) then
+    Stdlib.(!add_rules_callback ~path:sign.sign_path s rs)
 
 (** [add_rule sign s r] adds the new rule [r] to the symbol [s]. When the rule
     does not correspond to a symbol of signature [sign], it is stored in its

src/tool/indexing.ml

@@ -731,7 +731,7 @@ let index_term_and_subterms ~is_spine t item =
   List.sort_uniq cmp (subterms_to_index ~is_spine tn) in
  List.iter (fun (where,s) -> insert_rigid s (item where)) subterms
 
-let index_rule sym ({Core.Term.lhs=lhsargs ; rule_pos ; _} as rule) =
+let index_rule ~path sym ({Core.Term.lhs=lhsargs ; rule_pos ; _} as rule) =
  let rule_pos =
    match rule_pos with
     | None -> assert false (* this probably may happen, but it is BAD!
@@ -741,9 +741,6 @@ let index_rule sym ({Core.Term.lhs=lhsargs ; rule_pos ; _} as rule) =
  let lhs = Core.Term.add_args (Core.Term.mk_Symb sym) lhsargs in
  let rhs = rule.rhs in
  let get_relation = function | DB.Conclusion r -> r | _ -> assert false in
- let filename = Option.get rule_pos.fname in
- let filename = Lplib.String.remove_prefix "file://" filename in
- let path = Library.path_of_file Parsing.LpLexer.escape filename in
  let rule_name = (path,Common.Pos.to_string ~print_fname:false rule_pos) in
  index_term_and_subterms ~is_spine:false lhs
   (fun where -> ((rule_name,Some rule_pos),[Xhs(get_relation where,Lhs)])) ;
@@ -752,9 +749,9 @@ let index_rule sym ({Core.Term.lhs=lhsargs ; rule_pos ; _} as rule) =
 
 let _ =
  Stdlib.(Core.Sign.add_rules_callback :=
-   fun sym rules -> List.iter (index_rule sym) rules)
+   fun ~path sym rules -> List.iter (index_rule ~path sym) rules)
 
-let index_sym sym =
+let index_sym ~path sym =
  let qname = name_of_sym sym in
  (* Name *)
  if List.exists (fun ((sn,_),_) -> sn=qname)
@@ -771,7 +768,7 @@ let index_sym sym =
  (* InBody??? sym.sym_def : term option ref
     but all the subterms are too much; collect only the constants? *)
  (* Rules *)
- List.iter (index_rule sym) Timed.(!(sym.Core.Term.sym_rules))
+ List.iter (index_rule ~path sym) Timed.(!(sym.Core.Term.sym_rules))
 
 let _ = Stdlib.(Core.Sign.add_symbol_callback := index_sym)
 
@@ -784,13 +781,14 @@ let index_sign sign =
  Common.Logger.set_debug true "e" ;*)
  let syms = Timed.(!(sign.Core.Sign.sign_symbols)) in
  let deps = Timed.(!(sign.Core.Sign.sign_deps)) in
- Lplib.Extra.StrMap.iter (fun _ sym -> index_sym sym) syms ;
+ let path = sign.Core.Sign.sign_path in
+ Lplib.Extra.StrMap.iter (fun _ sym -> index_sym ~path sym) syms ;
  Common.Path.Map.iter
-  (fun path d ->
+  (fun p d ->
     Lplib.Extra.StrMap.iter
      (fun name sd ->
-       let sym = Core.Sign.find_qualified path name in
-       List.iter (index_rule sym) sd.Sign.rules)
+       let sym = Core.Sign.find_qualified p name in
+       List.iter (index_rule ~path sym) sd.Sign.rules)
      d.Sign.dep_symbols)
   deps