Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/kernel/   (Beweissystem des Inria Version 9.1.0©)  Datei vom 15.8.2025 mit Größe 1 kB image not shown  

Quelle  dune   Sprache: unbekannt

 
(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))

(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)))

[ Dauer der Verarbeitung: 0.22 Sekunden  (vorverarbeitet)  ]