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

Quelle  dune   Sprache: unbekannt

 
(library
 (name coqrun)
 (synopsis "Rocq's Kernel Abstract Reduction Machine [C implementation]")
 (public_name rocq-runtime.vm)
 (foreign_stubs
  (language c)
  (names rocq_fix_code rocq_float64 rocq_memory rocq_values rocq_interp)
  (flags :standard (:include %{project_root}/config/dune.c_flags))))

(deprecated_library_name
 (old_public_name coq-core.vm)
 (new_public_name rocq-runtime.vm))

(rule
 (targets rocq_instruct.h)
 (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe enum))))

(rule
 (targets rocq_jumptbl.h)
 (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe jump))))

(rule
 (targets rocq_arity.h)
 (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe arity))))

Messung V0.5
C=86 H=98 G=91

[ Dauer der Verarbeitung: 0.15 Sekunden  (vorverarbeitet)  ]