Skip to content

Commit 99eae36

Browse files
SkySkimmerSkySkimmer
committed
Enable warning 70 (missing mli), add mli files
I am tired of seeing compilation bottleneck on random grammar files
1 parent e2485bf commit 99eae36

File tree

109 files changed

+797
-285
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

109 files changed

+797
-285
lines changed

‎boot/path.mli

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
(************************************************************************)
2+
(* * The Coq Proof Assistant / The Coq Development Team *)
3+
(* v * Copyright INRIA, CNRS and contributors *)
4+
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
5+
(* \VV/ **************************************************************)
6+
(* // * This file is distributed under the terms of the *)
7+
(* * GNU Lesser General Public License Version 2.1 *)
8+
(* * (see LICENSE file for the text of the license) *)
9+
(************************************************************************)
10+
11+
(* Re-exported for convenience *)
12+
include module type of struct include Env.Path end

‎boot/util.mli

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
(************************************************************************)
2+
(* * The Coq Proof Assistant / The Coq Development Team *)
3+
(* v * Copyright INRIA, CNRS and contributors *)
4+
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
5+
(* \VV/ **************************************************************)
6+
(* // * This file is distributed under the terms of the *)
7+
(* * GNU Lesser General Public License Version 2.1 *)
8+
(* * (see LICENSE file for the text of the license) *)
9+
(************************************************************************)
10+
11+
val getenv_else : string -> (unit -> string) -> string
12+
13+
val check_file_else :
14+
dir:string -> file:string -> (unit -> string) -> string

‎clib/unicodetable.mli

+31
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
val lu : (int * int) list
2+
val ll : (int * int) list
3+
val lt : (int * int) list
4+
val mn : (int * int) list
5+
val mc : (int * int) list
6+
val me : (int * int) list
7+
val nd : (int * int) list
8+
val nl : (int * int) list
9+
val no : (int * int) list
10+
val zs : (int * int) list
11+
val zl : (int * int) list
12+
val zp : (int * int) list
13+
val cc : (int * int) list
14+
val cf : (int * int) list
15+
val cs : (int * int) list
16+
val co : (int * int) list
17+
val cn : (int * int) list
18+
val lm : (int * int) list
19+
val lo : (int * int) list
20+
val pc : (int * int) list
21+
val pd : (int * int) list
22+
val ps : (int * int) list
23+
val pe : (int * int) list
24+
val pi : (int * int) list
25+
val pf : (int * int) list
26+
val po : (int * int) list
27+
val sm : (int * int) list
28+
val sc : (int * int) list
29+
val sk : (int * int) list
30+
val so : (int * int) list
31+
val to_lower : ((int * int) * [> `Abs of int | `Delta of int ]) list

‎config/list_plugins.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ let plugins =
44

55
let () = Array.sort compare plugins
66

7-
let () =Array.iter (fun f ->
7+
let () = Array.iter (fun f ->
88
let f' = "plugins/"^f in
99
if Sys.is_directory f' && f.[0] <> '.' then print_endline f)
1010
plugins

‎config/list_plugins.mli

Whitespace-only changes.

‎coqpp/coqpp_lex.mli

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
(************************************************************************)
2+
(* * The Coq Proof Assistant / The Coq Development Team *)
3+
(* v * Copyright INRIA, CNRS and contributors *)
4+
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
5+
(* \VV/ **************************************************************)
6+
(* // * This file is distributed under the terms of the *)
7+
(* * GNU Lesser General Public License Version 2.1 *)
8+
(* * (see LICENSE file for the text of the license) *)
9+
(************************************************************************)
10+
11+
exception Lex_error of Coqpp_ast.loc * string
12+
13+
val loc : Lexing.lexbuf -> Coqpp_ast.loc
14+
15+
val token : Lexing.lexbuf -> Coqpp_parse.token

‎coqpp/coqpp_main.mli

Whitespace-only changes.

‎dev/bench/render_line_results.mli

Whitespace-only changes.

‎dev/bench/render_results.ml

-1
Original file line numberDiff line numberDiff line change
@@ -109,7 +109,6 @@ module CList = struct
109109
fold_left f h t
110110

111111
let min l = reduce Stdlib.min l
112-
let max l = reduce Stdlib.max l
113112

114113
end
115114
;;

‎dev/bench/render_results.mli

Whitespace-only changes.

‎dev/ci/user-overlays/17293-SkySkimmer-force-mli.sh

+3
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
overlay metacoq https://github.com/SkySkimmer/metacoq force-mli 17293
2+
3+
overlay serapi https://github.com/SkySkimmer/coq-serapi force-mli 17293

‎doc/plugin_tutorial/dune

+4
Original file line numberDiff line numberDiff line change
@@ -8,3 +8,7 @@
88
; ../../theories/Init/Prelude.vo)
99
; (action
1010
; (bash "make COQCORELIB=$(pwd)/../../ COQLIB=$(pwd)/../../")))
11+
12+
13+
(env
14+
(dev (flags :standard -w -70)))

‎doc/tools/docgram/doc_grammar.ml

-168
Original file line numberDiff line numberDiff line change
@@ -89,24 +89,6 @@ type gram = {
8989

9090
let sprintf = Printf.sprintf
9191

92-
let map_and_concat f ?(delim="") l =
93-
String.concat delim (List.map f l)
94-
95-
let rec db_output_prodn = function
96-
| Sterm s -> sprintf "(Sterm %s) " s
97-
| Snterm s -> sprintf "(Snterm %s) " s
98-
| Slist1 sym -> sprintf "(Slist1 %s) " (db_output_prodn sym)
99-
| Slist1sep (sym, sep) -> sprintf "(Slist1sep %s %s) " (db_output_prodn sep) (db_output_prodn sym)
100-
| Slist0 sym -> sprintf "(Slist0 %s) " (db_output_prodn sym)
101-
| Slist0sep (sym, sep) -> sprintf "(Slist0sep %s %s) " (db_output_prodn sep) (db_output_prodn sym)
102-
| Sopt sym -> sprintf "(Sopt %s) " (db_output_prodn sym)
103-
| Sparen prod -> sprintf "(Sparen %s) " (db_out_list prod)
104-
| Sprod prods -> sprintf "(Sprod %s) " (db_out_prods prods)
105-
| Sedit s -> sprintf "(Sedit %s) " s
106-
| Sedit2 (s, s2) -> sprintf "(Sedit2 %s %s) " s s2
107-
and db_out_list prod = sprintf "(%s)" (map_and_concat db_output_prodn prod)
108-
and db_out_prods prods = sprintf "( %s )" (map_and_concat ~delim:" | " db_out_list prods)
109-
11092
(* identify special chars that don't get a trailing space in output *)
11193
let omit_space s = List.mem s ["?"; "."; "#"]
11294

@@ -378,8 +360,6 @@ let pr_prods nt prods = (* duplicative *)
378360
prods;
379361
Printf.printf "]\n\n"
380362

381-
type fmt = [`MLG | `PRODLIST | `PRODN ]
382-
383363
(* print a subset of the grammar with nts in the specified order *)
384364
let print_in_order out g fmt nt_order hide =
385365
List.iter (fun nt ->
@@ -994,41 +974,6 @@ let map_name s =
994974
in
995975
good_name s
996976

997-
let rec gen_nt_name sym =
998-
let name_from_prod prod =
999-
let rec aux name sterm_name prod =
1000-
if name <> "" then name else
1001-
match prod with
1002-
| [] -> sterm_name
1003-
| Sterm s :: tl
1004-
| Snterm s :: tl ->
1005-
if good_name s <> "" then
1006-
aux (map_name s) sterm_name tl
1007-
else
1008-
aux name (map_name s) tl;
1009-
| sym :: tl->
1010-
aux (gen_nt_name sym) sterm_name tl
1011-
in
1012-
aux "" "" prod
1013-
in
1014-
1015-
let name = match sym with
1016-
| Sterm s -> map_name s
1017-
| Snterm s -> s
1018-
| Slist1 sym
1019-
| Slist1sep (sym, _)
1020-
| Slist0 sym
1021-
| Slist0sep (sym, _)
1022-
| Sopt sym ->
1023-
gen_nt_name sym
1024-
| Sparen slist ->
1025-
name_from_prod slist
1026-
| Sprod slistlist ->
1027-
name_from_prod (List.hd slistlist)
1028-
| _ -> ""
1029-
in
1030-
good_name name
1031-
1032977
(* create a new nt for LIST* or OPT with the specified name *)
1033978
let maybe_add_nt g insert_after name sym queue =
1034979
let empty = [Snterm "empty"] in
@@ -1104,17 +1049,6 @@ let maybe_add_nt g insert_after name sym queue =
11041049
end;
11051050
new_nt
11061051

1107-
let apply_merge g edit_map =
1108-
List.iter (fun b ->
1109-
let (from_nt, to_nt) = b in
1110-
let from_prods = NTMap.find from_nt !g.map in
1111-
List.iter (fun prod ->
1112-
try
1113-
ignore( get_first prod (NTMap.find to_nt !g.map));
1114-
with Not_found -> g_add_prod_after g None to_nt prod)
1115-
from_prods)
1116-
(NTMap.bindings edit_map)
1117-
11181052
let apply_rename_delete g edit_map =
11191053
List.iter (fun b -> let (nt, _) = b in
11201054
let prods = try NTMap.find nt !g.map with Not_found -> [] in
@@ -1358,11 +1292,6 @@ let nt_closure g start stops =
13581292
in
13591293
List.rev (nt_closure_r [] [start])
13601294

1361-
let header = "--------------------------------------------"
1362-
let nt_subset_in_orig_order g nts =
1363-
let subset = StringSet.of_list nts in
1364-
List.filter (fun nt -> StringSet.mem nt subset) !g.order
1365-
13661295
let index_of str list =
13671296
let rec index_of_r str list index =
13681297
match list with
@@ -1373,61 +1302,9 @@ let index_of str list =
13731302
in
13741303
index_of_r str list 0
13751304

1376-
exception IsNone
1377-
13781305
(* todo: raise exception for bad n? *)
13791306
let rec nthcdr n list = if n <= 0 then list else nthcdr (n-1) (List.tl list)
13801307

1381-
let pfx n list =
1382-
let rec pfx_r n res = function
1383-
| item :: tl -> if n < 0 then res else pfx_r (n-1) (item :: res) tl
1384-
| [] -> res
1385-
in
1386-
List.rev (pfx_r n [] list)
1387-
1388-
(* todo: adjust Makefile to include Option.ml/mli *)
1389-
let get_opt = function
1390-
| Some y -> y
1391-
| _ -> raise IsNone
1392-
1393-
let get_range g start end_ =
1394-
let starti, endi = get_opt (index_of start !g.order), get_opt (index_of end_ !g.order) in
1395-
pfx (endi - starti) (nthcdr starti !g.order)
1396-
1397-
let get_rangeset g start end_ = StringSet.of_list (get_range g start end_)
1398-
1399-
let check_range_consistency g start end_ =
1400-
let defined_list = get_range g start end_ in
1401-
let defined = StringSet.of_list defined_list in
1402-
let referenced = List.fold_left (fun set nt ->
1403-
let prods = NTMap.find nt !g.map in
1404-
let refs = List.concat (List.map nts_in_prod prods) in
1405-
StringSet.union set (StringSet.of_list refs))
1406-
StringSet.empty defined_list
1407-
in
1408-
let undef = StringSet.diff referenced defined in
1409-
let unused = StringSet.diff defined referenced in
1410-
if StringSet.cardinal unused > 0 || (StringSet.cardinal undef > 0) then begin
1411-
Printf.printf "\nFor range '%s' to '%s':\n External reference:" start end_;
1412-
StringSet.iter (fun nt -> Printf.printf " %s" nt) undef;
1413-
Printf.printf "\n";
1414-
if StringSet.cardinal unused > 0 then begin
1415-
Printf.printf " Unreferenced:";
1416-
StringSet.iter (fun nt -> Printf.printf " %s" nt) unused;
1417-
Printf.printf "\n"
1418-
end
1419-
end
1420-
1421-
(* print info on symbols with a single production of a single nonterminal *)
1422-
let check_singletons g =
1423-
NTMap.iter (fun nt prods ->
1424-
if List.length prods = 1 && !show_warn then
1425-
if List.length (remove_Sedit2 (List.hd prods)) = 1 then
1426-
warn "Singleton non-terminal, maybe SPLICE?: %s\n" nt
1427-
else
1428-
(*warn "Single production, maybe SPLICE?: %s\n" nt*) ())
1429-
!g.map
1430-
14311308
let report_bad_nts g file =
14321309
let all_nts_ref, all_nts_def = get_refdef_nts g in
14331310
let undef = StringSet.diff all_nts_ref all_nts_def in
@@ -1443,51 +1320,6 @@ let report_bad_nts g file =
14431320
if !show_warn then
14441321
List.iter (fun nt -> warn "%s: Unreachable symbol '%s'\n" file nt) unreachable
14451322

1446-
1447-
let report_info g symdef_map =
1448-
let num_prods = List.fold_left (fun sum nt -> let prods = NTMap.find nt !g.map in sum + (List.length prods))
1449-
0 !g.order
1450-
in
1451-
1452-
Printf.eprintf "\nstart symbols: %s\n" (String.concat " " start_symbols);
1453-
Printf.eprintf "%d nonterminals defined, %d productions\n" (NTMap.cardinal !g.map) num_prods;
1454-
Printf.eprintf "%d terminals\n" (List.length tokens);
1455-
1456-
Printf.eprintf "\nSymbols with multiple definition points in *.mlg:\n";
1457-
let bindings = List.sort (fun a b -> let (ak, _) = a and (bk, _) = b in
1458-
String.compare ak bk) (StringMap.bindings symdef_map) in
1459-
List.iter (fun b ->
1460-
let (k, v) = b in
1461-
if List.length v > 1 then begin
1462-
Printf.eprintf " %s: " k;
1463-
List.iter (fun f -> Printf.eprintf "%s " f) v;
1464-
Printf.eprintf "\n"
1465-
end)
1466-
bindings;
1467-
Printf.eprintf "\n"
1468-
1469-
1470-
1471-
[@@@ocaml.warning "-32"]
1472-
let rec dump prod =
1473-
match prod with
1474-
| hd :: tl -> let s = (match hd with
1475-
| Sterm s -> sprintf "Sterm %s" s
1476-
| Snterm s -> sprintf "Snterm \"%s\"" s
1477-
| Slist1 sym -> "Slist1"
1478-
| Slist0 sym -> "Slist0"
1479-
| Sopt sym -> "Sopt"
1480-
| Slist1sep _ -> "Slist1sep"
1481-
| Slist0sep _ -> "Slist0sep"
1482-
| Sparen sym_list -> "Sparen"
1483-
| Sprod sym_list_list -> "Sprod"
1484-
| Sedit _ -> "Sedit"
1485-
| Sedit2 _ -> "Sedit2") in
1486-
Printf.printf "%s " s;
1487-
dump tl
1488-
| [] -> Printf.printf "\n"
1489-
[@@@ocaml.warning "+32"]
1490-
14911323
let reorder_grammar eg reordered_rules file =
14921324
let og = g_empty () in
14931325
List.iter (fun rule ->

‎doc/tools/docgram/doc_grammar.mli

Whitespace-only changes.

‎dune

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
; Default flags for all Coq libraries.
22
(env
3-
(dev (flags :standard -w -9-27@60-70 \ -short-paths)
3+
(dev (flags :standard -w -9-27@60@70 \ -short-paths)
44
(coq (flags :standard -w +default)))
55
(release (flags :standard)
66
(ocamlopt_flags :standard -O3 -unbox-closures))

‎ide/coqide/configwin_messages.ml

-15
Original file line numberDiff line numberDiff line change
@@ -25,15 +25,6 @@
2525

2626
(** Module containing the messages of Configwin.*)
2727

28-
let software = "Configwin";;
29-
let version = "1.2";;
30-
31-
let html_config = "Configwin bindings configurator for html parameters"
32-
33-
let home = Option.default "" (Glib.get_home_dir ())
34-
35-
let mCapture = "Capture";;
36-
let mType_key = "Type key" ;;
3728
let mAdd = "Add";;
3829
let mRemove = "Remove";;
3930
let mUp = "Up";;
@@ -42,9 +33,3 @@ let mOk = "Ok";;
4233
let mCancel = "Cancel";;
4334
let mApply = "Apply";;
4435
let mValue = "Value"
45-
let mKey = "Key"
46-
47-
let shortcuts = "Shortcuts"
48-
let html_end = "End with"
49-
let html_begin = "Begin with"
50-

‎ide/coqide/configwin_messages.mli

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
val mAdd : string
2+
val mRemove : string
3+
val mUp : string
4+
val mEdit : string
5+
val mOk : string
6+
val mCancel : string
7+
val mApply : string
8+
val mValue : string

‎ide/coqide/configwin_types.ml ‎ide/coqide/configwin_types.mli

File renamed without changes.

‎ide/coqide/default_bindings_src.mli

+21
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
val logic : string
2+
val symbol : string
3+
val fraction : string
4+
val letter : string
5+
val greek_letter : string
6+
val asciiart : string
7+
val equivalence : string
8+
val order : string
9+
val circle : string
10+
val square : string
11+
val triangle : string
12+
val arrow : string
13+
val set : string
14+
val math : string
15+
val space : string
16+
val delimiter : string
17+
val miscellanea : string
18+
val bindings_set_1 : (string list * string * string list) list
19+
val bindings_set_2 : (string * string) list
20+
val priorities : (string * int) list
21+
val filename : string

‎ide/coqide/dune

+1
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,7 @@
2828
(wrapped false)
2929
(modules (:standard \ document idetop coqide_main default_bindings_src gen_gtk_platform
3030
shared shared_os_specific))
31+
(modules_without_implementation configwin_types)
3132
(foreign_stubs
3233
(language c)
3334
(names coqide_os_stubs))

‎ide/coqide/gen_gtk_platform.mli

Whitespace-only changes.

0 commit comments

Comments
 (0)