diff options
| author | Maxime Dénès | 2018-10-09 18:21:04 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-11-06 14:19:37 +0100 |
| commit | a1bdaf0635b5d5b9e007662f324dd526ba0fe8d3 (patch) | |
| tree | cc247d4ae7a66223add8ea189ca63125edd7d64e /checker/dune | |
| parent | 58f891c100d1a1821ed6385c1d06f9e0a77ecdac (diff) | |
[checker] Refactor by sharing code with the kernel
For historical reasons, the checker was duplicating a lot of code of the
kernel. The main differences I found were bug fixes that had not been
backported.
With this patch, the checker uses the kernel as a library to serve the
same purpose as before: validation of a `.vo` file, re-typechecking all
definitions a posteriori.
We also rename some files from the checker so that they don't clash with
kernel files.
Diffstat (limited to 'checker/dune')
| -rw-r--r-- | checker/dune | 29 |
1 files changed, 24 insertions, 5 deletions
diff --git a/checker/dune b/checker/dune index 5aff9211d7..35a35a1f82 100644 --- a/checker/dune +++ b/checker/dune @@ -1,7 +1,25 @@ -(rule (copy %{project_root}/kernel/names.ml names.ml)) -(rule (copy %{project_root}/kernel/names.mli names.mli)) -(rule (copy %{project_root}/kernel/esubst.ml esubst.ml)) -(rule (copy %{project_root}/kernel/esubst.mli esubst.mli)) +(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}.ml{,i}) + +; VM stuff + +(copy_files# + %{project_root}/kernel/byterun/{*.c,*.h}) ; Careful with bug https://github.com/ocaml/odoc/issues/148 ; @@ -12,7 +30,8 @@ (public_name coq.checklib) (synopsis "Coq's Standalone Proof Checker") (modules :standard \ coqchk votour) - (modules_without_implementation cic) + (modules_without_implementation cinstr nativeinstr) + (c_names coq_fix_code coq_memory coq_values coq_interp) (wrapped true) (libraries coq.lib)) |