Quelle dune Sprache: Text

(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.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.