summaryrefslogtreecommitdiff
path: root/dev/README
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /dev/README
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'dev/README')
-rw-r--r--dev/README54
1 files changed, 41 insertions, 13 deletions
diff --git a/dev/README b/dev/README
index a8811bea..0e40e820 100644
--- a/dev/README
+++ b/dev/README
@@ -1,21 +1,49 @@
-This directory contains informations and tools to help developping the
-Coq system
+This directory contains informations and tools to help developing the
+ Coq system
+ ======================
-TODO
-changements.txt
-header
-lisezmoi.txt
-style.txt
+Debugging and profiling (in current directory - see doc/debugging.txt)
+-----------------------
-Debugging and profiling
-=======================
+ocamldebug-coq: to launch ocaml debugger
-debugging.txt: help for debugging or profiling
-db: to install pretty-printers from ocaml debugger
+db: to install pretty-printers from ocaml debugger
base_db: to install raw pretty-printers from ocaml debugger
-ocamldebug-v7: to launch ocaml debugger
-include: to install pretty-printers from ocaml toplevel
+
+include: to install pretty-printers from ocaml toplevel
base_include: to install raw pretty-printers from ocaml toplevel
+
+vm_printers.ml, dev_printers.ml: ML pretty-printers for debugging
+
+
+Miscellaneous informations about the code (directory doc)
+-----------------------------------------
+
+changes.txt: (partial) per-version summary of the evolutions of Coq ML source
+style.txt: a few style recommendations for writing Coq ML files
+debugging.txt: help for debugging or profiling
universes.txt: help to debug universes
+translate.txt: help to use coq translator
+extensions.txt: some help about TACTIC EXTEND
+
+header: standard header for Coq ML files
+perf-analysis: analysis of perfs measured on the compilation of user contribs
+cic.dtd: official dtd of the calc. of ind. constr. for im/ex-portation
+
+
+Documentation of ML interfaces using tex (directory ocamlweb-doc)
+----------------------------------------
+
+go in directory and call "make"
+
+
+Other development tools (directory tools)
+-----------------------
+
univdot: produces a graph of CIC universes
+Makefile.dir: makefile dedicated to intensive work in a given directory
+Makefile.subdir: makefile dedicated to intensive work in a given subdirectory
+Makefile.devel: utilities to automatically launch coq in various states
+Makefile.common: used by other Makefiles
+objects.el: various development utilities at emacs level