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

Quelle  dune   Sprache: SML

 
(library
 (name config)
 (synopsis "Rocq Configuration Variables")
 (public_name rocq-runtime.config)
 (modules coq_config)
 (wrapped false))

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

(library
 (name byte_config)
 (synopsis "Rocq Configuration Variables (for bytecode only)")
 (public_name rocq-runtime.config.byte)
 (modules coq_byte_config)
 (wrapped false)
 (libraries compiler-libs.toplevel)
 (modes byte))

(deprecated_library_name
  (old_public_name coq-core.config.byte)
  (new_public_name rocq-runtime.config.byte))

(executable (name list_plugins) (modules list_plugins))
(rule (targets plugin_list)
  (deps (source_tree %{project_root}/plugins))
  (action (with-stdout-to %{targets} (chdir %{project_root} (run config/list_plugins.exe)))))

; add "-native-compiler yes" to the arguments of configure to enable native
(rule
 (targets coq_config.ml coq_byte_config.ml coq_config.py dune.c_flags)
 (mode fallback)
 (deps
   %{project_root}/dev/ocamldebug-coq.run
   %{project_root}/dev/header.c
   ; Needed to generate include lists for coq_makefile
   plugin_list)
 (action (chdir %{project_root} (run %{project_root}/tools/configure/configure.exe -quiet -relocatable))))

¤ Dauer der Verarbeitung: 0.13 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland






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.