aboutsummaryrefslogtreecommitdiff
path: root/dev/README
diff options
context:
space:
mode:
authorherbelin2006-05-23 21:51:59 +0000
committerherbelin2006-05-23 21:51:59 +0000
commite24d8149c3aefd11b03458b6f9b3e38ca454b07a (patch)
tree7c66dda6b63ea0c1f3e6e03259ef0b1609aca8b6 /dev/README
parentb65fd67d6210f480eed759d58422ca8c4da95eab (diff)
Restructuration dossier dev et mise à jour de certaines documentations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8856 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/README')
-rw-r--r--dev/README52
1 files changed, 39 insertions, 13 deletions
diff --git a/dev/README b/dev/README
index a8811beab7..a4ca8f334a 100644
--- a/dev/README
+++ b/dev/README
@@ -1,21 +1,47 @@
-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
+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