products/sources/formale Sprachen/Isabelle/Tools image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: dune   Sprache: SML

Original von: Coq©

; This is an ad-hoc rule to ease the migration, it should be handled
; natively by Dune in the future.
(rule
 (targets index-list.html)
 (deps
   make-library-index index-list.html.template hidden-files
   (source_tree %{project_root}/theories)
   (source_tree %{project_root}/plugins))
 (action
  (chdir %{project_root}
   ; On windows run will fail
   (bash "doc/stdlib/make-library-index doc/stdlib/index-list.html doc/stdlib/hidden-files"))))

(rule
  (targets html)
  (deps
   ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg
   (source_tree %{project_root}/theories)
   (source_tree %{project_root}/plugins)
   (:header %{project_root}/doc/common/styles/html/coqremote/header.html)
   (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html)
   ; For .glob files, should be gone when Coq Dune is smarter.
   (package coq))
 (action
  (progn
   (run mkdir -p html)
   (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq $(find %{project_root}/theories %{project_root}/plugins -name *.v)")
   (run mv html/index.html html/genindex.html)
   (with-stdout-to
     _index.html
    (progn (cat %{header}) (cat index-list.html) (cat %{footer})))
   (run cp _index.html html/index.html))))

(alias
 (name stdlib-html)
 (deps html))

¤ Dauer der Verarbeitung: 0.1 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




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.


Bot Zugriff