Merge pull request #225 from LPCIC/better-warnings

coq.warning

Changelog.md

@@ -2,9 +2,14 @@
 
 ## UNRELEASED
 
+### Typechecker
+- Warnings can be turned into errors by passing Coq `-w +elpi.typecheck`.
+
 ### API
 - New `coq.CS.db-for` to filter the CS db given a projection or a canonical
   value, or both.
+- New `coq.warning` like `coq.warn` but with a category and name, so that
+  the message can be silenced or turned into an error.
 
 ## [1.9.4] - 17-03-2021
 

coq-builtin.elpi

@@ -414,9 +414,15 @@ type canonical bool -> field-attribute. % default true, if field is named
 % [coq.say ...] Prints an info message
 external type coq.say variadic any prop.
 
-% [coq.warn ...] Prints a warning message
+% [coq.warn ...] Prints a generic warning message
 external type coq.warn variadic any prop.
 
+% [coq.warning Category Name ...] 
+% Prints a warning message with a Name an Category which can be used
+% to silence this warning or turn it into an error. See coqc -w connad
+% line option
+external type coq.warning string -> string -> variadic any prop.
+
 % [coq.error ...] Prints and *aborts* the program (it's a fatal error)
 external type coq.error variadic any prop.
 

elpi/coq-elpi-checker.elpi

@@ -17,6 +17,4 @@ error-concat [pr L X] R :- error-concat XS Rest, term_to_string L LS, R is LS ^
 error-concat [pr L X|XS] R :- error-concat XS Rest, term_to_string L LS, R is LS ^ " " ^ X ^ "\n" ^ Rest.
 
 :before "default-typechecking-warning"
-warning L M :- !, coq.warn L M.
-
-% vim:set ft=lprolog spelllang=:
+warning L M :- !, coq.warning "elpi" "elpi.typecheck" L M.

src/coq_elpi_builtins.ml

@@ -852,8 +852,32 @@ let coq_builtins =
   DocAbove);
 
   MLCode(Pred("coq.warn",
-    VariadicIn(unit_ctx, !> B.any, "Prints a warning message"),
+    VariadicIn(unit_ctx, !> B.any, "Prints a generic warning message"),
   (fun args ~depth _hyps _constraints state ->
+     let pp = pp ~depth in
+     let loc, args =
+       if args = [] then None, args
+       else
+         let x, args = List.hd args, List.tl args in
+         match E.look ~depth x with
+         | E.CData loc when API.RawOpaqueData.is_loc loc ->
+           Some (Coq_elpi_utils.to_coq_loc (API.RawOpaqueData.to_loc loc)), args
+         | _ -> None, x :: args
+     in
+     warning ?loc (pp2string (P.list ~boxed:true pp " ") args);
+     state, ()
+     )),
+  DocAbove);
+
+  MLCode(Pred("coq.warning",
+    In(B.string,"Category",
+    In(B.string,"Name",
+    VariadicIn(unit_ctx, !> B.any, {|
+Prints a warning message with a Name and Category which can be used
+to silence this warning or turn it into an error. See coqc -w commad
+line option|}))),
+  (fun category name args ~depth _hyps _constraints state ->
+     let warning = CWarnings.create ~name ~category Pp.str in
      let pp = pp ~depth in
      let loc, args =
        if args = [] then None, args

tests/test_API.v

@@ -169,7 +169,8 @@ Elpi Query lp:{{
 }}.
 
 Elpi Query lp:{{
-  coq.warn "this is a warning".
+  coq.warn "this is a generic warning",
+  coq.warning "category" "name"  "this is a warning with a name an category".
 }}.
 
 (****** locate **********************************)