indications pour les developpeurs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@231 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 57 insertions, 12 deletions

diff --git a/dev/changements.txt b/dev/changements.txt
index 538424d7fc..ab188cafb9 100644
--- a/dev/changements.txt
+++ b/dev/changements.txt
@@ -78,10 +78,10 @@ Changements divers
    directement le résultat du link du code
    => debuggage et profiling directs
 
- . il n'y a plus d'installation locale dans bin/
+ . il n'y a plus d'installation locale dans bin/$ARCH
  
  . #use "include.ml"  =>  #use "include"
    go()               =>  loop()
 
- . il y "make depend" et "make dependcamlp4" car ce dernier prend beaucoup
+ . il y a "make depend" et "make dependcamlp4" car ce dernier prend beaucoup
    de temps
diff --git a/dev/lisezmoi.txt b/dev/lisezmoi.txt
new file mode 100644
index 0000000000..eea7a0bc1f
--- /dev/null
+++ b/dev/lisezmoi.txt
@@ -0,0 +1,30 @@
+
+Debuggage
+=========
+
+   dans Emacs. nécessite le mode tuareg.
+   Coq doit être configuré avec -debug et -local (./configure -debug -local)
+
+   1. M-x camldebug
+   2. spécifier le binaire coqtop.byte
+   3. spécifier dev/ocamldebug-v7
+   4. source db  (pour avoir les pretty-printers)
+   5. poser ses points d'arrêts avec C-x C-a C-b (penser "add breakpoint")
+      directement dans le source ocaml
+   6. ensuite voir le man d'ocamldebug
+         run
+	 step
+	 next
+	 last
+	 print x
+	 ...
+
+
+Profiling
+=========
+
+   Coq doit être configuré avec -profile
+
+   1. Lancer Coq en natif, qui doit terminer normalement (utiliser Quit
+      ou l'option -batch)
+   2. gprof ./coqtop gmon.out
diff --git a/dev/ocamldebug-v7 b/dev/ocamldebug-v7
index bad484c41c..dc6c2279d4 100755
--- a/dev/ocamldebug-v7
+++ b/dev/ocamldebug-v7
@@ -2,18 +2,33 @@
 
 # wrap around ocamldebug for Coq
 
-export COQTOP=$constr/V7
+# export COQTOP=`coqtop -where`
+export COQTOP=/users/homepc89/jcf/coq/V7
+export COQLIB=$COQTOP
+export COQTH=$COQLIB/theories
 export CAMLP4LIB=`camlp4 -where`
 CAMLBIN=`which ocamlc`
 OCAMLDEBUG=`dirname $CAMLBIN`/ocamldebug
 
-exec $OCAMLDEBUG \
-	-I $CAMLP4LIB \
-	-I $COQTOP/lib \
-	-I $COQTOP/dev \
-	-I $COQTOP/kernel \
-	-I $COQTOP/parsing \
-        -I $COQTOP/toplevel \
-	$*
-
+args=""
+coqdebug="no"
+for op in $*
+    do case `basename $op` in
+	coq-debug-programs.out) 
+	    coqdebug="yes"
+	    args="-is programs.coq";;
+	coq*) coqdebug="yes";;
+       esac
+done
 
+case $coqdebug in
+    yes)
+	exec $OCAMLDEBUG \
+	-I $CAMLP4LIB \
+	-I $COQTOP/lib -I $COQTOP/kernel \
+	-I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \
+        -I $COQTOP/proofs -I $COQTOP/tactics \
+	-I $COQTOP/toplevel -I $COQTOP/dev \
+	$* $args;;
+    *) exec $OCAMLDEBUG $*;;
+esac