Merge PR #8961: dune: link kernel in checker instead of copying files

3 files changed, 3 insertions, 28 deletions

diff --git a/checker/dune b/checker/dune
index 3ab4f50d13..ee427d26c5 100644
--- a/checker/dune
+++ b/checker/dune
@@ -1,26 +1,3 @@
-(copy_files#
-  %{project_root}/kernel/{names,esubst,declarations,environ,constr,term,univ,evar,sorts,uGraph,context}.ml{,i})
-
-(copy_files#
-  %{project_root}/kernel/{mod_subst,vars,opaqueproof,conv_oracle,reduction,typeops,inductive,indtypes,declareops,type_errors}.ml{,i})
-
-(copy_files#
-  %{project_root}/kernel/{modops,mod_typing,}.ml{,i})
-
-(copy_files#
-  %{project_root}/kernel/{cClosure,cPrimitives,csymtable,vconv,vm,uint31,cemitcodes,vmvalues,cbytecodes,cinstr,retroknowledge,copcodes}.ml{,i})
-
-(copy_files#
-  %{project_root}/kernel/{cbytegen,clambda,nativeinstr,nativevalues,nativeconv,nativecode,nativelib,nativelibrary,nativelambda}.ml{,i})
-
-(copy_files#
-  %{project_root}/kernel/{subtyping,term_typing,safe_typing,entries,cooking,transparentState}.ml{,i})
-
-; VM stuff
-
-(copy_files#
-  %{project_root}/kernel/byterun/{*.c,*.h})
-
 ; Careful with bug https://github.com/ocaml/odoc/issues/148
 ;
 ; If we don't pack checker we will have a problem here due to
@@ -30,10 +7,8 @@
  (public_name coq.checklib)
  (synopsis "Coq's Standalone Proof Checker")
  (modules :standard \ coqchk votour)
- (modules_without_implementation cinstr nativeinstr)
- (c_names coq_fix_code coq_memory coq_values coq_interp)
  (wrapped true)
- (libraries coq.lib))
+ (libraries coq.kernel))
 
 (executable
  (name coqchk)
diff --git a/dev/dune b/dev/dune
index 7dfaa616b6..792da6254a 100644
--- a/dev/dune
+++ b/dev/dune
@@ -10,7 +10,7 @@
 (rule
   (targets dune-dbg)
   (deps dune-dbg.in
-        ../checker/main.bc
+        ../checker/coqchk.bc
         ../topbin/coqtop_byte_bin.bc
         ; This is not enough as the call to `ocamlfind` will fail :/
         top_printers.cma)
diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in
index 3f3df23fe1..80ad0500e0 100755
--- a/dev/dune-dbg.in
+++ b/dev/dune-dbg.in
@@ -3,7 +3,7 @@
 # Run in a proper install dune env.
 case $1 in
     checker)
-        exe=_build/default/checker/main.bc
+        exe=_build/default/checker/coqchk.bc
         ;;
     *)
         exe=_build/default/topbin/coqtop_byte_bin.bc