From 708d38aa324112e98ea21f5c5940e39b2ea253be Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Fri, 15 Sep 2023 17:12:46 +0200
Subject: [PATCH] [coq] Properly concatenate warnings

Thanks to @mituharu for the careful bug report.

Fixes #540
---
 CHANGES.md                  |  2 ++
 coq/workspace.ml            | 12 +++++++-----
 coq/workspace.mli           |  5 ++++-
 test/CoqProject/_CoqProject |  1 +
 test/CoqProject/test.v      |  6 ++++++
 5 files changed, 20 insertions(+), 6 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index 0b21f52c0..4813d2f9f 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -5,6 +5,8 @@
    improvements to goal pretty printing (@ejgallego, #530)
  - Added link to Python coq-lsp client by Pedro Carrot and Nuno
    Saavedra (@Nfsaavedra, #536)
+ - Properly concatenate warnings from _CoqProject (@ejgallego,
+   reported by @mituharu, #541, fixes #540)
 
 # coq-lsp 0.1.7: Just-in-time
 -----------------------------
diff --git a/coq/workspace.ml b/coq/workspace.ml
index a53ecbeeb..ffa96e2fb 100644
--- a/coq/workspace.ml
+++ b/coq/workspace.ml
@@ -34,16 +34,18 @@ module Warning : sig
   type t
 
   val make : string -> t
-  val apply : t -> unit
+
+  (** Adds new warnings to the list of current warnings *)
+  val apply : t list -> unit
 end = struct
   type t = string
 
   let make x = x
-  let to_string x = x
 
   let apply w =
-    let warn = CWarnings.get_flags () in
-    CWarnings.set_flags (warn ^ to_string w)
+    let old_warn = CWarnings.get_flags () in
+    let new_warn = String.concat "," w in
+    CWarnings.set_flags (old_warn ^ "," ^ new_warn)
 end
 
 type t =
@@ -236,7 +238,7 @@ let apply ~uri
     } =
   if debug then CDebug.set_flags "backtrace";
   Flags.apply flags;
-  List.iter Warning.apply warnings;
+  Warning.apply warnings;
   List.iter Mltop.add_ml_dir ml_include_path;
   findlib_init ~ml_include_path ~ocamlpath;
   List.iter Loadpath.add_vo_path vo_load_path;
diff --git a/coq/workspace.mli b/coq/workspace.mli
index 11cfedc80..829a99947 100644
--- a/coq/workspace.mli
+++ b/coq/workspace.mli
@@ -26,7 +26,10 @@ module Warning : sig
   type t
 
   val make : string -> t
-  val apply : t -> unit
+
+  (** Adds new warnings to the list of current warnings, the Coq API
+      here is a bit tricky... *)
+  val apply : t list -> unit
 end
 
 type t = private
diff --git a/test/CoqProject/_CoqProject b/test/CoqProject/_CoqProject
index 1f555a69c..da0de778b 100644
--- a/test/CoqProject/_CoqProject
+++ b/test/CoqProject/_CoqProject
@@ -2,5 +2,6 @@
 -Q . test
 
 -arg -w -arg -local-declaration
+-arg -w -arg +non-primitive-record
 
 test.v
diff --git a/test/CoqProject/test.v b/test/CoqProject/test.v
index 11151b3d6..ea6b2bcfa 100644
--- a/test/CoqProject/test.v
+++ b/test/CoqProject/test.v
@@ -1 +1,7 @@
 Variable (A : nat).
+
+Set Primitive Projections.
+
+Record a := { _ : nat }.
+
+Print Options.