Add rocqchk command and rocq check subcommand, move coqchk back t…

…o coq-core

checker/dune

@@ -6,20 +6,28 @@
  (name coq_checklib)
  (public_name rocq-runtime.checklib)
  (synopsis "Rocq's Standalone Proof Checker")
- (modules :standard \ coqchk votour)
+ (modules :standard \ rocqchk coqchk votour)
  (wrapped true)
  (libraries rocq-runtime.boot rocq-runtime.kernel))
 
 (deprecated_library_name
  (old_public_name coq-core.checklib)
  (new_public_name rocq-runtime.checklib))
 
+(executable
+ (name rocqchk)
+ (public_name rocqchk)
+ (modes exe byte)
+ (package rocq-runtime)
+ (modules rocqchk)
+ (flags :standard -open Coq_checklib)
+ (libraries coq_checklib))
+
 (executable
  (name coqchk)
  (public_name coqchk)
  (modes exe byte)
- ; Move to coq-checker?
- (package rocq-runtime)
+ (package coq-core)
  (modules coqchk)
  (flags :standard -open Coq_checklib)
  (libraries coq_checklib))

checker/rocqchk.ml

@@ -0,0 +1,2 @@
+
+let () = Coqchk_main.main ()

topbin/rocq.ml

@@ -23,6 +23,12 @@ let with_worker_gen opts basename args =
 let with_worker opts kind args =
   with_worker_gen opts "coqworker" (("--kind="^kind) :: args)
 
+let with_sibling_exe opts prog args =
+  let prog = System.get_toplevel_path prog in
+  let () = if opts.Rocqshim.debug_shim then Printf.eprintf "Using %s\n%!" prog in
+  let argv = Array.of_list (prog :: args) in
+  Rocqshim.exec_or_create_process prog argv
+
 let () =
   if Array.length Sys.argv < 2 then error_usage ();
 
@@ -38,6 +44,9 @@ let () =
   | ("top-with-drop"|"repl-with-drop") :: args -> with_worker_gen opts "coqworker_with_drop" args
   | "native-precompile" :: args -> with_worker_gen opts "rocqnative" args
 
+  (* public executables *)
+  | "check" :: args -> with_sibling_exe opts "rocqchk" args
+
   (* statically linked subcommands *)
   | ("preprocess-mlg"|"pp-mlg") :: args -> Coqpp_main.main args
   | "dep" :: args -> Coqdeplib.Rocqdep_main.main args