Merge branch 'Deducteam:master' into master

CHANGES.md

@@ -13,6 +13,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 
 - Induction tactic.
 
+### Changed
+
+- The export option `--requiring` does not require as argument a file with extension `.v` anymore: the argument must be a module name.
+
 ## 2.5.1 (2024-07-22)
 
 ### Added

doc/options.rst

@@ -122,7 +122,7 @@ In symbol declarations or definitions, parameters with no type are assumed to be
 
 It instructs Lambdapi to replace any occurrence of the unqualified identifier ``lp_id`` by ``coq_expr``, which can be any Coq expression. Example: `renaming.lp <https://github.com/Deducteam/lambdapi/blob/master/libraries/renaming.lp>`__.
 
-* ``--requiring <COQ_FILE>`` to add ``Require Import <COQ_FILE>`` at the beginning of the output. ``<COQ_FILE>`` usually needs to contain at least the following definitions:
+* ``--requiring <MODNAME>`` to add ``Require Import <MODNAME>`` at the beginning of the output. ``<MODNAME>.v`` usually needs to contain at least the following definitions:
 
 ::
 

src/export/coq.ml

@@ -354,9 +354,7 @@ let set_requiring : string -> unit = fun f -> require := Some f
 let print : ast -> unit = fun s ->
   let oc = stdout in
   begin match !require with
-    | Some f ->
-      string oc "Require Import ";
-      string oc (Filename.chop_extension f); string oc ".\n"
+  | Some f -> string oc ("Require Import "^f^".\n")
   | None -> ()
   end;
   ast oc s

src/lsp/lp_lsp.ml

@@ -235,18 +235,6 @@ let get_node_at_pos doc line pos =
       res
     ) doc.Lp_doc.nodes
 
-let rec get_goals ~doc ~line ~pos =
-  let node = get_node_at_pos doc line pos in
-  let goals = match node with
-    | None -> Some([], None)
-    | Some n ->
-        closest_before (line+1, pos) n.goals in
-  match goals with
-    | None -> begin match node with
-              | None   -> None
-              | Some _ -> get_goals ~doc ~line:(line-1) ~pos:0 end
-    | Some (v,_) -> Some v
-
 (** [get_first_error doc] returns the first error inferred from doc.logs *)
 let get_first_error doc =
   List.fold_left (fun acc b ->
@@ -262,6 +250,25 @@ let get_first_error doc =
                    (bpos.start_line, bpos.start_col) <= 0 then
           acc else Some b) None doc.Lp_doc.logs
 
+let rec get_goals ~doc ~line ~pos =
+  let (line,pos) =
+    match get_first_error doc with
+    | Some ((_,_), Some errpos) ->
+      let errpos = (errpos.start_line, errpos.start_col) in
+      if compare errpos (line, pos) <= 0 then errpos else (line, pos)
+    | _ -> (line,pos)
+  in
+  let node = get_node_at_pos doc line pos in
+  let goals = match node with
+    | None -> Some([], None)
+    | Some n ->
+        closest_before (line+1, pos) n.goals in
+  match goals with
+    | None -> begin match node with
+              | None   -> None
+              | Some _ -> get_goals ~doc ~line:(line-1) ~pos:0 end
+    | Some (v,_) -> Some v
+
 let get_logs ~doc ~line ~pos : string =
   (* DEBUG LOG START *)
   LIO.log_error "get_logs"
@@ -294,7 +301,7 @@ let get_logs ~doc ~line ~pos : string =
       (fun ((_,msg),loc) ->
          match loc with
          | Some Pos.{start_line; start_col; _}
-           when compare (start_line,start_col) end_limit < 0 -> Some msg
+           when compare (start_line,start_col) end_limit <= 0 -> Some msg
          | _ -> None)
       doc.Lp_doc.logs
   in
@@ -303,12 +310,6 @@ let get_logs ~doc ~line ~pos : string =
 let do_goals ofmt ~id params =
   let uri, line, pos = get_docTextPosition params in
   let doc = Hashtbl.find completed_table uri in
-  let line, pos = match get_first_error doc with
-    | Some ((_, _), Some loc) ->
-      let eline, epos = loc.start_line, loc.start_col in
-      if compare (eline, epos) (line, pos) <= 0 then
-        eline, epos else line, pos
-    | _ -> line, pos in
   let goals = get_goals ~doc ~line ~pos in
   let logs = get_logs ~doc ~line ~pos in
   let result = LSP.json_of_goals goals ~logs in