modifs des scripts de test auto

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

4 files changed, 35 insertions, 42 deletions

diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile
index 88823d6d72..2a29f866ac 100644
--- a/contrib/extraction/test/Makefile
+++ b/contrib/extraction/test/Makefile
@@ -19,7 +19,7 @@ CMONAMES=
 include .names.ml
 include .names.cmo
 
-all: allml .depend allcmo
+all: ml2v v2ml allml .depend allcmo
 
 allml: .names.ml $(MLNAMES)
 
@@ -38,23 +38,25 @@ allcmo: .names.cmo $(CMONAMES)
 	rm -f .names.cmo; \
 	sed -e "1s/ML/CMO/" -e "s/\.ml/.cmo/" < .names.ml > .names.cmo
 
-tree: 
-	cp -fur $(TOPDIR)/theories .; rm -f theories/*/*.vo theories/*/*/*.vo
+tree:
+	for f in `cd $(TOPDIR); find theories -name \*.v`; do \
+		mkdir -p `dirname $$f`; \
+		cp $(TOPDIR)/$$f $$f; \
+	done
 
+ml2v: ml2v.ml
+	ocamlc -o $@ $<
+
+v2ml: v2ml.ml
+	ocamlc -o $@ $< 
 
 %.cmo:%.ml
 	ocamlc $(INCL) -c -i $<
 
-%.ml: ml2v
+%.ml: 
 	./extract `./ml2v $@`
 
 clean: 
 	rm -f theories/*/*.ml theories/*/*.cm*
 
-ml2v: ml2v.ml
-	ocamlc -o $@ $<
-
-v2ml: v2ml.ml
-	ocamlc -o $@ $< 
-
 include .depend
diff --git a/contrib/extraction/test/extract b/contrib/extraction/test/extract
index 4b3da13712..1b0886a7e9 100755
--- a/contrib/extraction/test/extract
+++ b/contrib/extraction/test/extract
@@ -2,6 +2,7 @@
 rm -f /tmp/extr.v 
 d=`dirname $1`
 n=`basename $1 .v`
-echo "Cd \"$d\". Extraction Module $n. " > /tmp/extr.v;\
-coqtop -batch -require $n -load-vernac-source /tmp/extr.v 
+echo "Cd \"$d\". Extraction Module $n. " > /tmp/extr$$.v;\
+(../../../bin/coqtop.opt -batch -require $n -load-vernac-source /tmp/extr$$.v && rm -f /tmp/extr$$.v) || (rm -f /tmp/extr$$.v; exit 1)
+
 
diff --git a/contrib/extraction/test/ml2v.ml b/contrib/extraction/test/ml2v.ml
index 665aabba4a..f891b40ff0 100644
--- a/contrib/extraction/test/ml2v.ml
+++ b/contrib/extraction/test/ml2v.ml
@@ -1,17 +1,13 @@
-let main () = begin
-  let j = Array.length (Sys.argv) in
-  if j>0 then begin
-	let s = Sys.argv.(1) in
-	let b = Filename.chop_extension (Filename.basename s) in 
-	let b0 = String.sub b 0 1 in
-	let b1 = String.capitalize b0 in  
-	let b = String.sub b 1 ((String.length b) -1) in 
-	let d = Filename.dirname s
-	in print_string (d^"/["^b0^b1^"]"^b^".v");
-	print_newline()
-  end;
-  exit(0)	
-end;;	
-
-main();;
- 		
+let _ =
+  let j = Array.length Sys.argv in
+  if j > 0 then
+    let fml = Sys.argv.(1) in
+    let f = Filename.chop_extension fml in 
+    let fv = f ^ ".v" in
+    if Sys.file_exists fv then
+      print_endline fv
+    else
+      let d = Filename.dirname f in
+      let b = String.capitalize (Filename.basename f) in
+      let fv = Filename.concat d (b ^ ".v") in
+      print_endline fv
diff --git a/contrib/extraction/test/v2ml.ml b/contrib/extraction/test/v2ml.ml
index c106147bfb..0a28f60842 100644
--- a/contrib/extraction/test/v2ml.ml
+++ b/contrib/extraction/test/v2ml.ml
@@ -1,15 +1,9 @@
-let main () = begin
+let _ = 
   let j = Array.length (Sys.argv) in
-  if j>0 then begin
-	let s = Sys.argv.(1) in
-	let b = Filename.chop_extension (Filename.basename s) in 
-	let b = String.uncapitalize b in
-	let d = Filename.dirname s
-	in print_string (d^"/"^b^".ml");
-	print_newline()
-  end;
-  exit(0)	
-end;;	
+  if j>0 then 
+    let s = Sys.argv.(1) in
+    let b = Filename.chop_extension (Filename.basename s) in 
+    let b = String.uncapitalize b in
+    let d = Filename.dirname s in 
+    print_endline (Filename.concat d (b ^ ".ml"))
 
-main();;
-