[compiler] Tweaks to display

ejgallego · May 16, 2024 · 3609c48 · 3609c48
1 parent 0b976b4
commit 3609c48
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 20 deletions.
diff --git a/compiler/output.ml b/compiler/output.ml
@@ -56,16 +56,16 @@ let set_callbacks (display : Args.Display.t) =
   Fleche.Io.CallBack.set cb;
   cb
 
-let set_config ~perfData =
+let set_config ~perfData ~display =
   Fleche.Config.(
     v :=
       { !v with
         send_perf_data = perfData
       ; eager_diagnostics = false
-      ; show_coq_info_messages = true
-      ; show_notices_as_diagnostics = true
+      ; show_coq_info_messages = display = Args.Display.Verbose
+      ; show_notices_as_diagnostics = display = Args.Display.Verbose
       })
 
 let init display ~perfData =
-  set_config ~perfData;
+  set_config ~perfData ~display;
   set_callbacks display
diff --git a/coq/loader.ml b/coq/loader.ml
@@ -38,13 +38,15 @@ let check_package_exists fl_pkg =
 let map_serlib fl_pkg =
   let supported = match fl_pkg with
     (* Supported by serlib *)             (* directory   *)
+    | "coq-core.plugins.btauto"           (* btauto *)
     | "coq-core.plugins.cc"               (* cc  *)
     | "coq-core.plugins.extraction"       (* extraction  *)
     | "coq-core.plugins.firstorder"       (* firstorder  *)
     | "coq-core.plugins.funind"           (* funind      *)
     | "coq-core.plugins.ltac"             (* ltac        *)
     | "coq-core.plugins.ltac2"            (* ltac2       *)
     | "coq-core.plugins.micromega"        (* micromega   *)
+    | "coq-core.plugins.micromega_core"   (* micromega_core *)
     | "coq-core.plugins.ring"             (* ring        *)
     | "coq-core.plugins.ssreflect"        (* ssreflect   *)
     | "coq-core.plugins.ssrmatching"      (* ssrmatching *)

diff --git a/plugins/univdiff/main.ml b/plugins/univdiff/main.ml
@@ -54,6 +54,11 @@ let dump_univdiff ~io ~token ~(doc : Doc.t) =
   let uri_str = Lang.LUri.File.to_string_uri uri in
   let out_file = Lang.LUri.File.to_string_file uri ^ ".unidiff" in
   let lvl = Io.Level.info in
+  let ndiags = Doc.diags doc |> List.length in
+  let message =
+    Format.asprintf "[univdiff plugin] %d diags present for file..." ndiags
+  in
+  Io.Report.message ~io ~lvl ~message;
   let message =
     Format.asprintf "[univdiff plugin] dumping universe diff for %s ..." uri_str
   in

diff --git a/test/compiler/basic/run.t b/test/compiler/basic/run.t
@@ -107,22 +107,6 @@ Compile a dependent file without the dep being built
   b.v
   b.vo
   $ cat proj1/a.diags
-  {
-    "range": {
-      "start": { "line": 0, "character": 0 },
-      "end": { "line": 0, "character": 19 }
-    },
-    "severity": 4,
-    "message": "aa is defined"
-  }
-  {
-    "range": {
-      "start": { "line": 6, "character": 0 },
-      "end": { "line": 6, "character": 4 }
-    },
-    "severity": 4,
-    "message": "foo is defined"
-  }
   $ cat proj1/b.diags
   {
     "range": {