(library (name kernel) (synopsis "The Rocq Kernel") (public_name rocq-runtime.kernel) (wrapped false) (modules_without_implementation values declarations entries) (modules (:standard \ genOpcodeFiles uint63_31 uint63_63 float64_31 float64_63)) (libraries boot lib coqrun dynlink)) ; used by dune coq mode (deprecated_library_name (old_public_name coq-core.kernel) (new_public_name rocq-runtime.kernel)) (executable (name genOpcodeFiles) (modules genOpcodeFiles)) (rule (targets vmopcodes.ml) (action (with-stdout-to %{targets} (run ./genOpcodeFiles.exe copml)))) (rule (targets vmopcodes.mli) (action (with-stdout-to %{targets} (run ./genOpcodeFiles.exe copmli)))) (rule (targets uint63.ml) (deps (:gen-file uint63_%{ocaml-config:int_size}.ml)) (action (copy# %{gen-file} %{targets}))) (rule (targets float64.ml) (deps (:gen-file float64_%{ocaml-config:int_size}.ml)) (action (copy# %{gen-file} %{targets}))) (documentation (package rocq-runtime)) ; In dev profile, we check the kernel against a more strict set of ; warnings. (env (dev (flags :standard -w @a-4-40-42-44-50)))