[Pkg-ocaml-maint-commits] r5988 - in /trunk/packages/why/branches/lenny/debian: changelog patches/cpulimit.dpatch rules

dogguy-guest at users.alioth.debian.org dogguy-guest at users.alioth.debian.org
Tue Sep 16 15:35:22 UTC 2008 

Author: dogguy-guest
Date: Tue Sep 16 15:35:22 2008
New Revision: 5988

URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/?sc=1&rev=5988
Log:
Renaming dp into why-dp

Modified:
    trunk/packages/why/branches/lenny/debian/changelog
    trunk/packages/why/branches/lenny/debian/patches/cpulimit.dpatch
    trunk/packages/why/branches/lenny/debian/rules

Modified: trunk/packages/why/branches/lenny/debian/changelog
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/why/branches/lenny/debian/changelog?rev=5988&op=diff
==============================================================================
--- trunk/packages/why/branches/lenny/debian/changelog (original)
+++ trunk/packages/why/branches/lenny/debian/changelog Tue Sep 16 15:35:22 2008
@@ -1,6 +1,7 @@
 why (2.13-2) UNRELEASED; urgency=low
 
   * Using why-cpulimit instead of cpulimit Debian package, closes: 498485.
+  * Renaming 'dp' into 'why-dp', closes: #499140.
   * Remove unnecessary dependency : cpulimit.
 
  -- Mehdi Dogguy <dogguy at pps.jussieu.fr>  Tue, 16 Sep 2008 14:49:14 +0200

Modified: trunk/packages/why/branches/lenny/debian/patches/cpulimit.dpatch
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/why/branches/lenny/debian/patches/cpulimit.dpatch?rev=5988&op=diff
==============================================================================
--- trunk/packages/why/branches/lenny/debian/patches/cpulimit.dpatch (original)
+++ trunk/packages/why/branches/lenny/debian/patches/cpulimit.dpatch Tue Sep 16 15:35:22 2008
@@ -1,23 +1,33 @@
 #! /bin/sh /usr/share/dpatch/dpatch-run
 ## cpulimit.dpatch by Mehdi Dogguy <dogguy at pps.jussieu.fr>
 ##
-## DP: Using why's version of cpulimit.
+## DP: Using why's version of cpulimit and renaming 'dp' into 'why-dp'.
 
 @DPATCH@
-diff -urNad 2.13-1~/Makefile.in 2.13-1/Makefile.in
---- 2.13-1~/Makefile.in	2008-05-28 16:55:38.000000000 +0200
-+++ 2.13-1/Makefile.in	2008-09-16 14:11:59.000000000 +0200
-@@ -148,7 +148,7 @@
+diff -urNad lenny~/Makefile.in lenny/Makefile.in
+--- lenny~/Makefile.in	2008-05-28 16:55:38.000000000 +0200
++++ lenny/Makefile.in	2008-09-16 17:31:39.000000000 +0200
+@@ -147,8 +147,8 @@
+ STATICBINARY=bin/why.static
  WHY2HTML=bin/why2html.$(OCAMLBEST)
  RVMERGE=bin/rv_merge.$(OCAMLBEST)
- DP=bin/dp.$(OCAMLBEST)
+-DP=bin/dp.$(OCAMLBEST)
 -CPULIMIT=bin/cpulimit
++DP=bin/why-dp.$(OCAMLBEST)
 +CPULIMIT=bin/why-cpulimit
  WHYOBFUSCATOR=bin/why-obfuscator.$(OCAMLBEST)
  WHYSTAT=bin/why-stat.$(OCAMLBEST)
  SIMPLIFY2WHY=bin/simplify2why.$(OCAMLBEST)
-@@ -537,7 +537,7 @@
- bin/dp.opt: $(DPCMX)
+@@ -531,13 +531,13 @@
+         tools/calldp.cmo tools/dp.cmo
+ DPCMX = $(DPCMO:.cmo=.cmx)
+ 
+-bin/dp.byte: $(DPCMO)
++bin/why-dp.byte: $(DPCMO)
+ 	$(OCAMLC) $(BFLAGS) -o $@ unix.cma $^
+ 
+-bin/dp.opt: $(DPCMX)
++bin/why-dp.opt: $(DPCMX)
  	$(OCAMLOPT) $(OFLAGS) -o $@ unix.cmxa $^
  
 -bin/cpulimit: tools/cpulimit.c
@@ -25,27 +35,158 @@
  	$(CC) -o $@ $^
  
  bin/rv_merge.byte: tools/rv_merge.ml
-@@ -669,7 +669,7 @@
+@@ -668,8 +668,8 @@
+ 	cp -f $(KRAKATOA) $(BINDIR)/krakatoa$(EXE)
  	cp -f bin/gwhy.sh $(BINDIR)/gwhy
  	cp -f $(WHY2HTML) $(BINDIR)/why2html$(EXE)
- 	cp -f $(DP) $(BINDIR)/dp$(EXE)
+-	cp -f $(DP) $(BINDIR)/dp$(EXE)
 -	cp -f $(CPULIMIT) $(BINDIR)/cpulimit$(EXE)
++	cp -f $(DP) $(BINDIR)/why-dp$(EXE)
 +	cp -f $(CPULIMIT) $(BINDIR)/why-cpulimit$(EXE)
  	cp -f $(RVMERGE) $(BINDIR)/rv_merge$(EXE)
  	cp -f $(WHYOBFUSCATOR) $(BINDIR)/why-obfuscator$(EXE)
  	cp -f $(WHYSTAT) $(BINDIR)/why-stat$(EXE)
-@@ -1036,7 +1036,7 @@
+@@ -1035,8 +1035,8 @@
+ 	rm -f bin/rv_merge.opt bin/rv_merge.byte
  	rm -f bin/why-stat.opt bin/why-stat.byte
  	rm -f bin/why2html.opt bin/why2html.byte
- 	rm -f bin/dp.opt bin/dp.byte
+-	rm -f bin/dp.opt bin/dp.byte
 -	rm -f bin/cpulimit
++	rm -f bin/why-dp.opt bin/why-dp.byte
 +	rm -f bin/why-cpulimit
  	rm -f lib/coq*/*.vo lib/coq*/*~
  	rm -f $(GENERATED)
  	make -C atp clean
-diff -urNad 2.13-1~/tools/calldp.ml 2.13-1/tools/calldp.ml
---- 2.13-1~/tools/calldp.ml	2008-05-28 16:55:38.000000000 +0200
-+++ 2.13-1/tools/calldp.ml	2008-09-16 14:11:10.000000000 +0200
+diff -urNad lenny~/c/cmake.ml lenny/c/cmake.ml
+--- lenny~/c/cmake.ml	2008-05-28 16:55:37.000000000 +0200
++++ lenny/c/cmake.ml	2008-09-16 17:31:39.000000000 +0200
+@@ -107,12 +107,12 @@
+ 	 Coptions.libdir;
+ 
+        fprintf fmt "simplify: %a@\n" (print_files simplify) targets;
+-       fprintf fmt "\t@@echo 'Running Simplify on proof obligations' && (dp -timeout $(TIMEOUT) $^)@\n@\n";
++       fprintf fmt "\t@@echo 'Running Simplify on proof obligations' && (why-dp -timeout $(TIMEOUT) $^)@\n@\n";
+        fprintf fmt "simplify/%%_why.sx: why/%s_spec.why why/%%.why@\n" f;
+        fprintf fmt "\t@@echo 'why -simplify [...] why/$*.why' && $(WHY) -simplify -no-simplify-prelude -dir  simplify $(CADULIB)/why/$(CADULIBFILE) why/%s_spec.why why/$*.why@\n@\n" f;
+        
+        fprintf fmt "ergo: %a@\n" (print_files ergo) targets;
+-       fprintf fmt "\t@@echo 'Running Ergo on proof obligations' && (dp -timeout $(TIMEOUT) $^)@\n@\n";
++       fprintf fmt "\t@@echo 'Running Ergo on proof obligations' && (why-dp -timeout $(TIMEOUT) $^)@\n@\n";
+        fprintf fmt "why/%%_why.sx: why/%s_spec.why why/%%.why@\n" f;
+        fprintf fmt "\t@@echo 'why -why [...] why/$*.why' && $(WHY) -why -dir why $(CADULIB)/why/$(CADULIBFILE) why/%s_spec.why why/$*.why@\n@\n" f;
+ 
+@@ -129,32 +129,32 @@
+ 
+ 
+        fprintf fmt "cvcl: %a@\n@\n" (print_files cvcl) targets;
+-       fprintf fmt "\t@@echo 'Running CVC Lite on proof obligations' && (dp -timeout $(TIMEOUT) $^)@\n@\n";
++       fprintf fmt "\t@@echo 'Running CVC Lite on proof obligations' && (why-dp -timeout $(TIMEOUT) $^)@\n@\n";
+        fprintf fmt "cvcl/%%_why.cvc: why/%s_spec.why why/%%.why@\n" f;
+        fprintf fmt "\t@@echo 'why -cvcl [...] why/$*.why' && $(WHY) -cvcl --encoding sstrat -dir cvcl $(CADULIB)/why/$(CADULIBFILE) why/%s_spec.why why/$*.why@\n@\n" f;
+        
+        fprintf fmt "harvey: %a@\n" (print_files harvey) targets;
+-       fprintf fmt "\t@@echo 'Running haRVey on proof obligations' && (dp -timeout $(TIMEOUT) $^)@\n@\n";
++       fprintf fmt "\t@@echo 'Running haRVey on proof obligations' && (why-dp -timeout $(TIMEOUT) $^)@\n@\n";
+        fprintf fmt "harvey/%%_why.rv: why/%s_spec.why why/%%.why@\n" f;
+        fprintf fmt "\t@@echo 'why -harvey [...] why/$*.why' && $(WHY) -harvey -dir harvey $(CADULIB)/why/$(CADULIBFILE) why/%s_spec.why why/$*.why@\n@\n" f;
+        
+        fprintf fmt "zenon: %a@\n" (print_files zenon) targets;
+-       fprintf fmt "\t@@echo 'Running Zenon on proof obligations' && (dp -timeout $(TIMEOUT) $^)@\n@\n";
++       fprintf fmt "\t@@echo 'Running Zenon on proof obligations' && (why-dp -timeout $(TIMEOUT) $^)@\n@\n";
+        fprintf fmt "zenon/%%_why.znn: why/%s_spec.why why/%%.why@\n" f;
+        fprintf fmt "\t@@echo 'why -zenon [...] why/$*.why' && $(WHY) -zenon -dir zenon $(CADULIB)/why/$(CADULIBFILE) why/%s_spec.why why/$*.why@\n@\n" f;
+        
+        fprintf fmt "smtlib: %a@\n" (print_files smtlib) targets;
+-       fprintf fmt "\t@@echo 'Running Yices on proof obligations' && (dp -timeout $(TIMEOUT) $^)@\n@\n";
++       fprintf fmt "\t@@echo 'Running Yices on proof obligations' && (why-dp -timeout $(TIMEOUT) $^)@\n@\n";
+        fprintf fmt "smtlib/%%_why.smt: why/%s_spec.why why/%%.why@\n" f;
+        fprintf fmt "\t@@echo 'why -smtlib [...] why/$*.why' && $(WHY) -smtlib --encoding sstrat -exp all   -dir smtlib $(CADULIB)/why/$(CADULIBFILE) why/%s_spec.why why/$*.why@\n@\n" f;
+        
+        fprintf fmt "z3: %a@\n" (print_files z3) targets;
+-       fprintf fmt "\t@@echo 'Running Z3 on proof obligations' && (dp -smt-solver z3 -timeout $(TIMEOUT) $^)@\n@\n";
++       fprintf fmt "\t@@echo 'Running Z3 on proof obligations' && (why-dp -smt-solver z3 -timeout $(TIMEOUT) $^)@\n@\n";
+        fprintf fmt "z3/%%_why.smt: why/%s_spec.why why/%%.why@\n" f;
+        fprintf fmt "\t@@echo 'why -smtlib [...] why/$*.why' && $(WHY) -smtlib --encoding sstrat -exp all   -dir z3 $(CADULIB)/why/$(CADULIBFILE) why/%s_spec.why why/$*.why@\n@\n" f;
+ 
+        fprintf fmt "cvc3: %a@\n" (print_files cvc3) targets;
+-       fprintf fmt "\t@@echo 'Running CVC3 on proof obligations' && (dp -smt-solver cvc3 -timeout $(TIMEOUT) $^)@\n@\n";
++       fprintf fmt "\t@@echo 'Running CVC3 on proof obligations' && (why-dp -smt-solver cvc3 -timeout $(TIMEOUT) $^)@\n@\n";
+        fprintf fmt "cvc3/%%_why.smt: why/%s_spec.why why/%%.why@\n" f;
+        fprintf fmt "\t@@echo 'why -smtlib [...] why/$*.why' && $(WHY) -smtlib --encoding sstrat -exp all   -dir cvc3 $(CADULIB)/why/$(CADULIBFILE) why/%s_spec.why why/$*.why@\n@\n" f;
+ 
+diff -urNad lenny~/examples/Makefile.common lenny/examples/Makefile.common
+--- lenny~/examples/Makefile.common	2008-05-28 16:55:39.000000000 +0200
++++ lenny/examples/Makefile.common	2008-09-16 17:31:39.000000000 +0200
+@@ -9,19 +9,19 @@
+ dp: simplify cvcl
+ 
+ simplify: $(VO:_valid.vo=_why.sx)
+-	dp -timeout 10 $^  2>/dev/null
++	why-dp -timeout 10 $^  2>/dev/null
+ 
+ yices: $(VO:_valid.vo=_why.smt)
+-	dp -timeout 10 $^  2>/dev/null
++	why-dp -timeout 10 $^  2>/dev/null
+ 
+ zenon: $(VO:_valid.vo=_why.znn)
+-	dp -timeout 10 $^ 2>/dev/null
++	why-dp -timeout 10 $^ 2>/dev/null
+ 
+ cvcl: $(VO:_valid.vo=_why.cvc)
+-	dp -timeout 10 $^  2>/dev/null
++	why-dp -timeout 10 $^  2>/dev/null
+ 
+ harvey: $(VO:_valid.vo=_why.rv)
+-	dp -timeout 10 $^  2>/dev/null
++	why-dp -timeout 10 $^  2>/dev/null
+ 
+ %_valid.v %_why.v: %.mlw $(WHY)
+ 	$(WHY) $(WHYOPTIONS) $<
+diff -urNad lenny~/jc/jc_make.ml lenny/jc/jc_make.ml
+--- lenny~/jc/jc_make.ml	2008-05-28 16:55:37.000000000 +0200
++++ lenny/jc/jc_make.ml	2008-09-16 17:31:39.000000000 +0200
+@@ -112,32 +112,32 @@
+ 	 Jc_options.libdir;
+ 
+        fprintf fmt "simplify: %a@\n" (print_files simplify) targets;
+-       fprintf fmt "\t@@echo 'Running Simplify on proof obligations' && (dp -timeout $(TIMEOUT) $^)@\n@\n";
++       fprintf fmt "\t@@echo 'Running Simplify on proof obligations' && (why-dp -timeout $(TIMEOUT) $^)@\n@\n";
+        fprintf fmt "simplify/%%_why.sx: why/%%.why@\n";
+        fprintf fmt "\t@@echo 'why -simplify [...] why/$*.why' && $(WHY) -simplify -no-simplify-prelude -dir simplify $(JESSIELIBFILE) why/$*.why@\n@\n";
+        
+        fprintf fmt "ergo: %a@\n" (print_files ergo) targets;
+-       fprintf fmt "\t@@echo 'Running Ergo on proof obligations' && (dp -timeout $(TIMEOUT) $^)@\n@\n";
++       fprintf fmt "\t@@echo 'Running Ergo on proof obligations' && (why-dp -timeout $(TIMEOUT) $^)@\n@\n";
+        fprintf fmt "why/%%_why.why: why/%%.why@\n";
+        fprintf fmt "\t@@echo 'why --why [...] why/$*.why' && $(WHY) --why -dir why $(JESSIELIBFILE) why/$*.why@\n@\n";
+        
+        fprintf fmt "cvcl: %a@\n@\n" (print_files cvcl) targets;
+-       fprintf fmt "\t@@echo 'Running CVC Lite on proof obligations' && (dp -timeout $(TIMEOUT) $^)@\n@\n";
++       fprintf fmt "\t@@echo 'Running CVC Lite on proof obligations' && (why-dp -timeout $(TIMEOUT) $^)@\n@\n";
+        fprintf fmt "cvcl/%%_why.cvc: why/%%.why@\n";
+        fprintf fmt "\t@@echo 'why -cvcl [...] why/$*.why' && $(WHY) -cvcl -dir cvcl $(JESSIELIBFILE) why/$*.why@\n@\n";
+        
+        fprintf fmt "harvey: %a@\n" (print_files harvey) targets;
+-       fprintf fmt "\t@@echo 'Running haRVey on proof obligations' && (dp -timeout $(TIMEOUT) $^)@\n@\n";
++       fprintf fmt "\t@@echo 'Running haRVey on proof obligations' && (why-dp -timeout $(TIMEOUT) $^)@\n@\n";
+        fprintf fmt "harvey/%%_why.rv: why/%%.why@\n";
+        fprintf fmt "\t@@echo 'why -harvey [...] why/$*.why' && $(WHY) -harvey -dir harvey $(JESSIELIBFILE) why/$*.why@\n@\n";
+        
+        fprintf fmt "zenon: %a@\n" (print_files zenon) targets;
+-       fprintf fmt "\t@@echo 'Running Zenon on proof obligations' && (dp -timeout $(TIMEOUT) $^)@\n@\n";
++       fprintf fmt "\t@@echo 'Running Zenon on proof obligations' && (why-dp -timeout $(TIMEOUT) $^)@\n@\n";
+        fprintf fmt "zenon/%%_why.znn: why/%%.why@\n";
+        fprintf fmt "\t@@echo 'why -zenon [...] why/$*.why' && $(WHY) -zenon -dir zenon $(JESSIELIBFILE) why/$*.why@\n@\n";
+        
+        fprintf fmt "smtlib: %a@\n" (print_files smtlib) targets;
+-       fprintf fmt "\t@@echo 'Running Yices on proof obligations' && (dp -timeout $(TIMEOUT) $^)@\n@\n";
++       fprintf fmt "\t@@echo 'Running Yices on proof obligations' && (why-dp -timeout $(TIMEOUT) $^)@\n@\n";
+        fprintf fmt "smtlib/%%_why.smt: why/%%.why@\n";
+        fprintf fmt "\t@@echo 'why -smtlib [...] why/$*.why' && $(WHY) -smtlib --encoding sstrat --exp goal -dir smtlib $(JESSIELIBFILE) why/$*.why@\n@\n";
+        
+diff -urNad lenny~/tools/calldp.ml lenny/tools/calldp.ml
+--- lenny~/tools/calldp.ml	2008-05-28 16:55:38.000000000 +0200
++++ lenny/tools/calldp.ml	2008-09-16 17:31:39.000000000 +0200
 @@ -67,7 +67,7 @@
    let t0 = Unix.times () in
    if debug then Format.eprintf "command line: %s at ." cmd;
@@ -55,3 +196,15 @@
    let ret = Sys.command cmd in
    let t1 = Unix.times () in
    let cpu_time = t1.Unix.tms_cutime -. t0.Unix.tms_cutime in
+diff -urNad lenny~/tools/dp.ml lenny/tools/dp.ml
+--- lenny~/tools/dp.ml	2008-05-28 16:55:38.000000000 +0200
++++ lenny/tools/dp.ml	2008-09-16 17:31:56.000000000 +0200
+@@ -59,7 +59,7 @@
+     "-smt-solver", Arg.String set_smt_solver, "<solver>";
+   ]
+ 
+-let usage = "usage: dp [options] files.{why,rv,znn,cvc,cvc.all,sx,sx.all,smt,smt.all}"
++let usage = "usage: why-dp [options] files.{why,rv,znn,cvc,cvc.all,sx,sx.all,smt,smt.all}"
+ let () = Arg.parse spec (fun s -> Queue.push s files) usage 
+ 
+ let () = 

Modified: trunk/packages/why/branches/lenny/debian/rules
URL: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/why/branches/lenny/debian/rules?rev=5988&op=diff
==============================================================================
--- trunk/packages/why/branches/lenny/debian/rules (original)
+++ trunk/packages/why/branches/lenny/debian/rules Tue Sep 16 15:35:22 2008
@@ -59,7 +59,6 @@
 	dh_installdirs
 
 	$(MAKE) prefix=$(CURDIR)/debian/why/usr install COQLIB=$(CURDIR)/debian/why/usr/lib/coq
-	mv $(CURDIR)/debian/why/usr/bin/dp $(CURDIR)/debian/why/usr/bin/why-dp
 
 # Build architecture-independent files here.
 binary-indep: build install

More information about the Pkg-ocaml-maint-commits mailing list