Quellcode-Bibliothek dune Sprache: Cobol

(library
(name rocqshim)
(public_name rocq-runtime.rocqshim)
(synopsis "Rocq support for finding and exec-ing subcommands")
(wrapped false) ; no point repeating the Rocqshim name
(modules rocqshim)
(libraries boot unix findlib))

(executable
(public_name rocq)
(package rocq-runtime)
(modules rocq)
(modes exe byte)
; we statically link the "small" subcommands instead of having separate binaries
(libraries rocqshim coqdeplib coqpp coqdoclib rocqwc rocqworkmgr rocqtex rocqmakefile))

(install
(section bin)
(package rocq-runtime)
(files (rocq.bc as rocq.byte)))

(executable
(name coqtop_bin)
(public_name coqtop)
(package coq-core)
(modules coqtop_bin)
(libraries rocqshim))

(executable
(name coqtop_byte_bin)
(public_name coqtop.byte)
(package coq-core)
(modules coqtop_byte_bin)
(libraries rocqshim))

(executable
(name coqc_bin)
(public_name coqc)
(package coq-core)
(modules coqc_bin)
(libraries rocqshim))

(executable
(name rocqnative)
(modules rocqnative)
(libraries rocq-runtime.kernel)
(modes exe byte) ; NB byte not installed, just exists for debugger
(link_flags -linkall))

(executable
(name coqnative)
(public_name coqnative)
(package coq-core)
(modules coqnative)
(libraries rocqshim))

; Workers
(executable
(name rocqworker)
(modules rocqworker)
(modes exe byte)
(libraries rocq-runtime.toplevel))
; Adding -ccopt -flto to links options could be interesting, however,
; it doesn't work on Windows

(executable
(name rocqworker_with_drop)
(modules rocqworker_with_drop)
(modes byte)
(libraries compiler-libs.toplevel rocq-runtime.config.byte rocq-runtime.toplevel rocq-runtime.dev findlib.top))

(install
(section libexec)
(package rocq-runtime)
(files
  (rocqworker.exe as rocqworker)
  (rocqworker.bc as rocqworker.byte)
  (rocqworker_with_drop.bc as rocqworker_with_drop)
  (rocqnative.exe as rocqnative)))

¤ 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.0.15Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

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.