diff options
| author | herbelin | 2006-05-23 21:51:59 +0000 |
|---|---|---|
| committer | herbelin | 2006-05-23 21:51:59 +0000 |
| commit | e24d8149c3aefd11b03458b6f9b3e38ca454b07a (patch) | |
| tree | 7c66dda6b63ea0c1f3e6e03259ef0b1609aca8b6 /dev/README | |
| parent | b65fd67d6210f480eed759d58422ca8c4da95eab (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/README | 52 |
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 |
