Quelle dune Sprache: Coq

; The easiest way to generate a portable absolute path is to use OCaml
; itself to print it
(executable
(name ocaml_pwd)
(modules ocaml_pwd))

(env
(dev (flags :standard -w -70)))

(rule
(targets test_suite_config.inc)
(action (with-stdout-to %{targets} (run tools/coq_config_to_make.exe %{bin:coqc}))))

(rule
(targets summary.log)
(deps
   ; File that should be promoted.
   misc/universes/all_stdlib.v
   ; Configure for test-suite
   test_suite_config.inc
   ; when TIMED is set, used to print the timing table
   ../tools/make-one-time-file.py
   ../tools/TimeFileMaker.py
   ; For the changelog test
   ../config/coq_config.py
   (source_tree doc/changelog)
   (package rocq-runtime)
   (package coq-core)
   (package rocq-core)
   (package coqide-server) ; For fake_ide
   (package rocq-devtools) ; For bench-render
   (source_tree .))
   ; Finer-grained dependencies would look like this and be generated
   ; by coqdep; that would allow tests to be run incrementally.
   ; ../tools/CoqMakefile.in
   ; ../theories/Init/Prelude.vo
   ; %{bin:coqc}
   ; %{bin:coq_makefile}
   ; %{bin:fake_ide}
(action
  (progn
   (bash "make -j %{env:NJOBS=2} PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}"))))

¤ Dauer der Verarbeitung: 0.11 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.