[tools] Checkdecls tool for Coq blueprints

Thanks to Andrej Bauer for the hint!

CHANGES.md

@@ -66,6 +66,8 @@
    configurable with different methods; moreover, `petanque/run` can
    compute some extra data like state hashing without a round-trip
    (@ejgallego @gbdrt, #779)
+ - [tools] New tool `checkdecls` for Coq blueprint, inspired by the
+   Lean version (#785, @ejgallego, Andrej Bauer, Patrick Massot)
 
 # coq-lsp 0.1.10: Hasta el 40 de Mayo _en effect_...
 ----------------------------------------------------

tools/checkdecls/driver.ml

@@ -0,0 +1,90 @@
+let err_fmt = Format.err_formatter
+let pf fmt = Format.kfprintf (fun fmt -> Format.pp_print_flush fmt ()) fmt
+
+let coq_init ~debug =
+  let load_module = Dynlink.loadfile in
+  let load_plugin = Coq.Loader.plugin_handler None in
+  Coq.Init.(coq_init { debug; load_module; load_plugin })
+
+let workspace_init ~token ~debug ~cmdline ~roots =
+  let roots = if List.length roots < 1 then [ Sys.getcwd () ] else roots in
+  let default = Coq.Workspace.default ~debug ~cmdline in
+  ( default
+  , List.map
+      (fun dir -> (dir, Coq.Workspace.guess ~token ~cmdline ~debug ~dir))
+      roots )
+
+(* Stdlib.Int.max requires OCaml 4.13 *)
+let int_max x y = if x >= y then x else y
+let max = List.fold_left int_max 0
+
+(* We capture all the exns, bad people *)
+let locate_decl decl =
+  try
+    let qid = Libnames.qualid_of_string decl in
+    Ok (Nametab.locate_constant qid)
+  with
+  | Not_found -> Error (Format.asprintf "%s not found\n" decl)
+  | exn ->
+    let iexn = Exninfo.capture exn in
+    let exn_msg = CErrors.iprint iexn |> Pp.string_of_ppcmds in
+    Error exn_msg
+
+let pp_lp = function
+  | Loadpath.Error.LibNotFound -> "LibNotFound"
+  | Loadpath.Error.LibUnmappedDir -> "LibUnmappedDir"
+
+(* EJGA: also check if the location info is available *)
+let location_enabled = false
+
+let do_decl decl =
+  let open Coq.Compat.Result.O in
+  let* cr = locate_decl decl in
+  if location_enabled then
+    let dp = Names.Constant.modpath cr |> Names.ModPath.dp in
+    let* m = Coq.Module.make dp |> Result.map_error pp_lp in
+    let id = Names.Constant.label cr |> Names.Label.to_string in
+    let* _loc_info = Coq.Module.find m id in
+    Ok ()
+  else Ok ()
+
+let do_decl decl =
+  (* pf err "decl for: %s" decl; *)
+  match do_decl decl with
+  | Ok () ->
+    (* pf err "decl found! %s" decl; *)
+    0
+  | Error err ->
+    pf err_fmt "Constant %s not found [err: %s]" decl err;
+    1
+
+let do_decls file =
+  Coq.Compat.Ocaml_414.In_channel.(with_open_text file input_all)
+  |> String.split_on_char '\n'
+  |> List.filter (fun s -> not (CString.is_empty s))
+  |> List.map do_decl |> max
+
+let do_decls ws files =
+  let intern = Vernacinterp.fs_intern in
+  let uri =
+    Lang.LUri.(of_string "file:///fake.v" |> File.of_uri) |> Result.get_ok
+  in
+  let () = Coq.Workspace.apply ~intern ~uri ws in
+  List.map do_decls files
+
+let do_decls ~token st ws files =
+  let f files = do_decls ws files in
+  Coq.State.in_state ~token ~st ~f files
+
+let go ~cmdline ~roots ~debug files =
+  Coq.Limits.select_best None;
+  Coq.Limits.start ();
+  let token = Coq.Limits.Token.create () in
+  let root_state = coq_init ~debug in
+  let default, _ws = workspace_init ~token ~debug ~cmdline ~roots in
+  match do_decls ~token root_state default files with
+  | { r = Interrupted; feedback = _ } -> 2
+  | { r = Completed (Ok outs); feedback = _ } -> max outs
+  | { r = Completed (Error _); feedback = _ } ->
+    pf err_fmt "critical error!";
+    222

tools/checkdecls/driver.mli

@@ -0,0 +1,6 @@
+val go :
+     cmdline:Coq.Workspace.CmdLine.t
+  -> roots:string list
+  -> debug:bool
+  -> string list
+  -> int

tools/checkdecls/dune

@@ -0,0 +1,4 @@
+(executable
+ (name main)
+ (public_name checkdecls)
+ (libraries coq cmdliner))

tools/checkdecls/main.ml

@@ -0,0 +1,70 @@
+(* Flèche Coq compiler / checkdecls for Coq-blueprints *)
+
+let cd_main roots debug files coqlib coqcorelib ocamlpath rload_path load_path
+    require_libraries =
+  let vo_load_path = rload_path @ load_path in
+  let ml_include_path = [] in
+  let args = [] in
+  let cmdline =
+    { Coq.Workspace.CmdLine.coqlib
+    ; coqcorelib
+    ; ocamlpath
+    ; vo_load_path
+    ; ml_include_path
+    ; args
+    ; require_libraries
+    }
+  in
+  Driver.go ~cmdline ~roots ~debug files
+
+open Cmdliner
+
+(****************************************************************************)
+let file : string list Term.t =
+  let doc = "File(s) to compile" in
+  Arg.(value & pos_all string [] & info [] ~docv:"FILES" ~doc)
+
+module Exit_codes = struct
+  let missing_id : Cmd.Exit.info =
+    let doc = "An input identifier was not found" in
+    Cmd.Exit.info ~doc 1
+
+  let stopped : Cmd.Exit.info =
+    let doc =
+      "The document was not fully checked: this is often due to a timeout, \
+       interrupt, or resource limit."
+    in
+    Cmd.Exit.info ~doc 2
+
+  let uri_failed : Cmd.Exit.info =
+    let doc =
+      "[INTERNAL] There was an internal error setting up the Coq workspace"
+    in
+    Cmd.Exit.info ~doc 222
+end
+
+let cd_cmd : int Cmd.t =
+  let doc = "CheckDecls for Coq" in
+  let man =
+    [ `S "DESCRIPTION"
+    ; `P "checkdecls checker"
+    ; `S "USAGE"
+    ; `P "See the documentation of blueprints"
+    ]
+  in
+  (* let version = Fleche.Version.server in *)
+  let version = "0.1" in
+  let fcc_term =
+    let open Coq.Args in
+    Term.(
+      const cd_main $ roots $ debug $ file $ coqlib $ coqcorelib $ ocamlpath
+      $ rload_paths $ qload_paths $ ri_from)
+  in
+  let exits = Exit_codes.[ missing_id; stopped; uri_failed ] in
+  Cmd.(v (Cmd.info "checkdecls" ~exits ~version ~doc ~man) fcc_term)
+
+let main () =
+  let ecode = Cmd.eval' cd_cmd in
+  exit ecode
+
+let () = main ()

tools/checkdecls/main.mli

@@ -0,0 +1 @@
+(* empty interface *)