From f88063f9ec21eb110921ef54b322f5b2fa9d6fb4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Wed, 12 Jun 2024 19:33:00 +0200
Subject: [PATCH] [tools] Checkdecls tool for Coq blueprints

Co-authored-by: Andrej Bauer <Andrej.Bauer@andrej.com>
---
 CHANGES.md                   |  2 +
 tools/checkdecls/driver.ml   | 97 ++++++++++++++++++++++++++++++++++++
 tools/checkdecls/driver.mli  |  6 +++
 tools/checkdecls/dune        |  4 ++
 tools/checkdecls/main.ml     | 70 ++++++++++++++++++++++++++
 tools/checkdecls/main.mli    |  1 +
 tools/checkdecls/tests/dune  |  5 ++
 tools/checkdecls/tests/run.t | 32 ++++++++++++
 8 files changed, 217 insertions(+)
 create mode 100644 tools/checkdecls/driver.ml
 create mode 100644 tools/checkdecls/driver.mli
 create mode 100644 tools/checkdecls/dune
 create mode 100644 tools/checkdecls/main.ml
 create mode 100644 tools/checkdecls/main.mli
 create mode 100644 tools/checkdecls/tests/dune
 create mode 100644 tools/checkdecls/tests/run.t

diff --git a/CHANGES.md b/CHANGES.md
index 801654be..33ca26fc 100644
--- a/CHANGES.md
+++ b/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_...
 ----------------------------------------------------
diff --git a/tools/checkdecls/driver.ml b/tools/checkdecls/driver.ml
new file mode 100644
index 00000000..c6ad20ac
--- /dev/null
+++ b/tools/checkdecls/driver.ml
@@ -0,0 +1,97 @@
+(************************************************************************)
+(* Flèche => checkdecls support for Proof blueprint                     *)
+(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
+(* Copyright 2019-2024 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
+(* Written by: Andrej Bauaer, Emilio J. Gallego Arias                   *)
+(************************************************************************)
+
+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 in name table" decl)
+  | exn ->
+    let iexn = Exninfo.capture exn in
+    let exn_msg = CErrors.iprint iexn |> Pp.string_of_ppcmds in
+    Error (Format.asprintf "internal Coq error: %s" 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 "Error when processing input %s [%s]@\n" 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
diff --git a/tools/checkdecls/driver.mli b/tools/checkdecls/driver.mli
new file mode 100644
index 00000000..726d4bc3
--- /dev/null
+++ b/tools/checkdecls/driver.mli
@@ -0,0 +1,6 @@
+val go :
+     cmdline:Coq.Workspace.CmdLine.t
+  -> roots:string list
+  -> debug:bool
+  -> files:string list
+  -> int
diff --git a/tools/checkdecls/dune b/tools/checkdecls/dune
new file mode 100644
index 00000000..e0539fed
--- /dev/null
+++ b/tools/checkdecls/dune
@@ -0,0 +1,4 @@
+(executable
+ (name main)
+ (public_name checkdecls)
+ (libraries coq cmdliner))
diff --git a/tools/checkdecls/main.ml b/tools/checkdecls/main.ml
new file mode 100644
index 00000000..47f1b0ee
--- /dev/null
+++ b/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 files : string list Term.t =
+  let doc = "Files with list of identifiers to check" in
+  Arg.(non_empty & pos_all non_dir_file [] & 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 $ files $ 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 ()
diff --git a/tools/checkdecls/main.mli b/tools/checkdecls/main.mli
new file mode 100644
index 00000000..b64034d8
--- /dev/null
+++ b/tools/checkdecls/main.mli
@@ -0,0 +1 @@
+(* empty interface *)
diff --git a/tools/checkdecls/tests/dune b/tools/checkdecls/tests/dune
new file mode 100644
index 00000000..e373eff8
--- /dev/null
+++ b/tools/checkdecls/tests/dune
@@ -0,0 +1,5 @@
+(cram
+ (deps
+  ; For the coq-lsp plugins to be built, in case we need it
+  (package coq-lsp)
+  %{bin:checkdecls}))
diff --git a/tools/checkdecls/tests/run.t b/tools/checkdecls/tests/run.t
new file mode 100644
index 00000000..1678e465
--- /dev/null
+++ b/tools/checkdecls/tests/run.t
@@ -0,0 +1,32 @@
+General tests for checkdecls
+
+Error when not input:
+
+  $ checkdecls
+  checkdecls: required argument FILES is missing
+  Usage: checkdecls [OPTION]… FILES…
+  Try 'checkdecls --help' for more information.
+  [124]
+
+Error when file doesn't exists:
+
+  $ checkdecls where_i_am.txt
+
+Simple test with one file, succeed
+
+  $ echo Coq.Init.Nat.add > clist
+  $ echo Coq.Init.Peano.plus_n_O >> clist
+  $ checkdecls clist
+  $ echo $?
+  0
+
+Simple test with one file, fail
+
+  $ echo Coq.Init.Peano.not_a_constant >> clist
+  $ echo Coq.Init.Nat.not_a_theorem >> clist
+  $ checkdecls clist
+  Error when processing input Coq.Init.Peano.not_a_constant [Coq.Init.Peano.not_a_constant not found in name table]
+  Error when processing input Coq.Init.Nat.not_a_theorem [Coq.Init.Nat.not_a_theorem not found in name table]
+  [1]
+  $ echo $?
+  0