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 <[EMAIL PROTECTED]> 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 <[EMAIL PROTECTED]>
##
-## 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: [EMAIL PROTECTED]" (print_files simplify)
targets;
+- fprintf fmt "\t@@echo 'Running Simplify on proof obligations' && (dp
-timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
++ fprintf fmt "\t@@echo 'Running Simplify on proof obligations' &&
(why-dp -timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
+ fprintf fmt "simplify/%%_why.sx: why/%s_spec.why why/[EMAIL
PROTECTED]" f;
+ fprintf fmt "\t@@echo 'why -simplify [...] why/$*.why' && $(WHY)
-simplify -no-simplify-prelude -dir simplify $(CADULIB)/why/$(CADULIBFILE)
why/%s_spec.why why/[EMAIL PROTECTED]@\n" f;
+
+ fprintf fmt "ergo: [EMAIL PROTECTED]" (print_files ergo) targets;
+- fprintf fmt "\t@@echo 'Running Ergo on proof obligations' && (dp
-timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
++ fprintf fmt "\t@@echo 'Running Ergo on proof obligations' && (why-dp
-timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
+ fprintf fmt "why/%%_why.sx: why/%s_spec.why why/[EMAIL PROTECTED]" f;
+ fprintf fmt "\t@@echo 'why -why [...] why/$*.why' && $(WHY) -why -dir
why $(CADULIB)/why/$(CADULIBFILE) why/%s_spec.why why/[EMAIL PROTECTED]@\n" f;
+
+@@ -129,32 +129,32 @@
+
+
+ fprintf fmt "cvcl: [EMAIL PROTECTED]@\n" (print_files cvcl) targets;
+- fprintf fmt "\t@@echo 'Running CVC Lite on proof obligations' && (dp
-timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
++ fprintf fmt "\t@@echo 'Running CVC Lite on proof obligations' &&
(why-dp -timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
+ fprintf fmt "cvcl/%%_why.cvc: why/%s_spec.why why/[EMAIL PROTECTED]" f;
+ fprintf fmt "\t@@echo 'why -cvcl [...] why/$*.why' && $(WHY) -cvcl
--encoding sstrat -dir cvcl $(CADULIB)/why/$(CADULIBFILE) why/%s_spec.why
why/[EMAIL PROTECTED]@\n" f;
+
+ fprintf fmt "harvey: [EMAIL PROTECTED]" (print_files harvey) targets;
+- fprintf fmt "\t@@echo 'Running haRVey on proof obligations' && (dp
-timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
++ fprintf fmt "\t@@echo 'Running haRVey on proof obligations' && (why-dp
-timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
+ fprintf fmt "harvey/%%_why.rv: why/%s_spec.why why/[EMAIL PROTECTED]"
f;
+ fprintf fmt "\t@@echo 'why -harvey [...] why/$*.why' && $(WHY) -harvey
-dir harvey $(CADULIB)/why/$(CADULIBFILE) why/%s_spec.why why/[EMAIL
PROTECTED]@\n" f;
+
+ fprintf fmt "zenon: [EMAIL PROTECTED]" (print_files zenon) targets;
+- fprintf fmt "\t@@echo 'Running Zenon on proof obligations' && (dp
-timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
++ fprintf fmt "\t@@echo 'Running Zenon on proof obligations' && (why-dp
-timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
+ fprintf fmt "zenon/%%_why.znn: why/%s_spec.why why/[EMAIL PROTECTED]"
f;
+ fprintf fmt "\t@@echo 'why -zenon [...] why/$*.why' && $(WHY) -zenon
-dir zenon $(CADULIB)/why/$(CADULIBFILE) why/%s_spec.why why/[EMAIL
PROTECTED]@\n" f;
+
+ fprintf fmt "smtlib: [EMAIL PROTECTED]" (print_files smtlib) targets;
+- fprintf fmt "\t@@echo 'Running Yices on proof obligations' && (dp
-timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
++ fprintf fmt "\t@@echo 'Running Yices on proof obligations' && (why-dp
-timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
+ fprintf fmt "smtlib/%%_why.smt: why/%s_spec.why why/[EMAIL PROTECTED]"
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/[EMAIL PROTECTED]@\n" f;
+
+ fprintf fmt "z3: [EMAIL PROTECTED]" (print_files z3) targets;
+- fprintf fmt "\t@@echo 'Running Z3 on proof obligations' && (dp
-smt-solver z3 -timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
++ fprintf fmt "\t@@echo 'Running Z3 on proof obligations' && (why-dp
-smt-solver z3 -timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
+ fprintf fmt "z3/%%_why.smt: why/%s_spec.why why/[EMAIL PROTECTED]" 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/[EMAIL PROTECTED]@\n" f;
+
+ fprintf fmt "cvc3: [EMAIL PROTECTED]" (print_files cvc3) targets;
+- fprintf fmt "\t@@echo 'Running CVC3 on proof obligations' && (dp
-smt-solver cvc3 -timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
++ fprintf fmt "\t@@echo 'Running CVC3 on proof obligations' && (why-dp
-smt-solver cvc3 -timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
+ fprintf fmt "cvc3/%%_why.smt: why/%s_spec.why why/[EMAIL PROTECTED]" 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/[EMAIL PROTECTED]@\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: [EMAIL PROTECTED]" (print_files simplify)
targets;
+- fprintf fmt "\t@@echo 'Running Simplify on proof obligations' && (dp
-timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
++ fprintf fmt "\t@@echo 'Running Simplify on proof obligations' &&
(why-dp -timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
+ fprintf fmt "simplify/%%_why.sx: why/[EMAIL PROTECTED]";
+ fprintf fmt "\t@@echo 'why -simplify [...] why/$*.why' && $(WHY)
-simplify -no-simplify-prelude -dir simplify $(JESSIELIBFILE) why/[EMAIL
PROTECTED]@\n";
+
+ fprintf fmt "ergo: [EMAIL PROTECTED]" (print_files ergo) targets;
+- fprintf fmt "\t@@echo 'Running Ergo on proof obligations' && (dp
-timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
++ fprintf fmt "\t@@echo 'Running Ergo on proof obligations' && (why-dp
-timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
+ fprintf fmt "why/%%_why.why: why/[EMAIL PROTECTED]";
+ fprintf fmt "\t@@echo 'why --why [...] why/$*.why' && $(WHY) --why
-dir why $(JESSIELIBFILE) why/[EMAIL PROTECTED]@\n";
+
+ fprintf fmt "cvcl: [EMAIL PROTECTED]@\n" (print_files cvcl) targets;
+- fprintf fmt "\t@@echo 'Running CVC Lite on proof obligations' && (dp
-timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
++ fprintf fmt "\t@@echo 'Running CVC Lite on proof obligations' &&
(why-dp -timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
+ fprintf fmt "cvcl/%%_why.cvc: why/[EMAIL PROTECTED]";
+ fprintf fmt "\t@@echo 'why -cvcl [...] why/$*.why' && $(WHY) -cvcl
-dir cvcl $(JESSIELIBFILE) why/[EMAIL PROTECTED]@\n";
+
+ fprintf fmt "harvey: [EMAIL PROTECTED]" (print_files harvey) targets;
+- fprintf fmt "\t@@echo 'Running haRVey on proof obligations' && (dp
-timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
++ fprintf fmt "\t@@echo 'Running haRVey on proof obligations' && (why-dp
-timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
+ fprintf fmt "harvey/%%_why.rv: why/[EMAIL PROTECTED]";
+ fprintf fmt "\t@@echo 'why -harvey [...] why/$*.why' && $(WHY) -harvey
-dir harvey $(JESSIELIBFILE) why/[EMAIL PROTECTED]@\n";
+
+ fprintf fmt "zenon: [EMAIL PROTECTED]" (print_files zenon) targets;
+- fprintf fmt "\t@@echo 'Running Zenon on proof obligations' && (dp
-timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
++ fprintf fmt "\t@@echo 'Running Zenon on proof obligations' && (why-dp
-timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
+ fprintf fmt "zenon/%%_why.znn: why/[EMAIL PROTECTED]";
+ fprintf fmt "\t@@echo 'why -zenon [...] why/$*.why' && $(WHY) -zenon
-dir zenon $(JESSIELIBFILE) why/[EMAIL PROTECTED]@\n";
+
+ fprintf fmt "smtlib: [EMAIL PROTECTED]" (print_files smtlib) targets;
+- fprintf fmt "\t@@echo 'Running Yices on proof obligations' && (dp
-timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
++ fprintf fmt "\t@@echo 'Running Yices on proof obligations' && (why-dp
-timeout $(TIMEOUT) $^)@[EMAIL PROTECTED]";
+ fprintf fmt "smtlib/%%_why.smt: why/[EMAIL PROTECTED]";
+ fprintf fmt "\t@@echo 'why -smtlib [...] why/$*.why' && $(WHY) -smtlib
--encoding sstrat --exp goal -dir smtlib $(JESSIELIBFILE) why/[EMAIL
PROTECTED]@\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: [EMAIL PROTECTED]" 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
_______________________________________________
Pkg-ocaml-maint-commits mailing list
[email protected]
http://lists.alioth.debian.org/mailman/listinfo/pkg-ocaml-maint-commits
