[Pkg-ocaml-maint-commits] [SCM] why packaging branch, master, updated. debian/2.19+dfsg-2-17-g9832da6

Sun Jan 10 22:34:40 UTC 2010

The following commit has been merged in the master branch:
commit 30edb457360fddfdfadd66eff7a59d1757e217a8
Author: Mehdi Dogguy <mehdi at debian.org>
Date:   Sun Jan 10 19:01:26 2010 +0100

    Various changes

diff --git a/debian/changelog b/debian/changelog
index f0c059e..9bd5e5e 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,8 +1,12 @@
 why (2.23+dfsg-1) UNRELEASED; urgency=low
 
   * New upstream release
+    + Remove makefile.in.dpatch (fixed upstream)
+    + Remove jessie_lib.dpatch (not needed anymore)
+    + Needs ocamlgraph 1.3
   * Fix detection of Alt-Ergo (Closes: #552776).
   * Set filter-pristine-tar to True in debian/gbp.conf
+  * Remove libjessie-ocaml-dev which is no longer user by Frama-C
   * Update copyright file
 
  -- Mehdi Dogguy <mehdi at debian.org>  Sun, 10 Jan 2010 18:20:23 +0100
diff --git a/debian/clean b/debian/clean
index cf48e91..b2e7907 100644
--- a/debian/clean
+++ b/debian/clean
@@ -24,5 +24,3 @@ mix/mix_parser.output
 regtest.opt
 tools/simplify_parser.output
 tools/toolstat_pars.output
-debian/libjessie-ocaml-dev.install
-debian/META
diff --git a/debian/control b/debian/control
index 63b0817..163a08a 100644
--- a/debian/control
+++ b/debian/control
@@ -15,7 +15,8 @@ Build-Depends:
   liblablgtk2-ocaml-dev (>= 2.12.0-3),
   coq (>= 8.2.pl1),
   libfloat-coq (>= 1:8.2-1.2-3),
-  libocamlgraph-ocaml-dev (>= 1.1),
+  libocamlgraph-ocaml-dev (>= 1.3),
+  frama-c-nox,
   dpatch
 Standards-Version: 3.8.2
 Homepage: http://why.lri.fr/
@@ -54,17 +55,6 @@ Description: Examples of programs certified with Why
  .
  This package contains examples of programs verified using Why.
 
-Package: libjessie-ocaml-dev
-Architecture: any
-Depends:
-  ocaml-nox-${F:OCamlABI},
-  ${misc:Depends}
-Section: ocaml
-Description: Jessie library for C code analysis
- Jessie library, from Why certification tool, is useful for deductive
- verification. It is based on weakest precondition computation techniques
- and allows to prove that C functions satisfy their specification.
-
 Package: libwhy-coq
 Architecture: all
 Depends:
diff --git a/debian/libjessie-ocaml-dev.NEWS b/debian/libjessie-ocaml-dev.NEWS
deleted file mode 100644
index 6f25ba9..0000000
--- a/debian/libjessie-ocaml-dev.NEWS
+++ /dev/null
@@ -1,8 +0,0 @@
-libjessie-ocaml-dev (2.18.dfsg-4) unstable; urgency=low
-
-  This package was created to allow frama-c to link against Why.
-  By default, frama-c use jc.cm{o,x} when linking. Thus, support for
-  jc.cm{x,}a is dropped. These files are replaced by jc.cm{o,x}.
-  META file is updated accordingly.
-
- -- Mehdi Dogguy <dogguy at pps.jussieu.fr>  Wed, 20 May 2009 15:42:47 +0200
diff --git a/debian/libjessie-ocaml-dev.install.in b/debian/libjessie-ocaml-dev.install.in
deleted file mode 100644
index e488b74..0000000
--- a/debian/libjessie-ocaml-dev.install.in
+++ /dev/null
@@ -1,5 +0,0 @@
-jc/jc.cmo @OCamlStdlibDir@/jessie/
-jc/jc.cmi @OCamlStdlibDir@/jessie/
-OPT: jc/jc.o @OCamlStdlibDir@/jessie/
-OPT: jc/jc.cmx @OCamlStdlibDir@/jessie/
-debian/META @OCamlStdlibDir@/jessie/
diff --git a/debian/patches/00list b/debian/patches/00list
index e9c6887..3036b44 100644
--- a/debian/patches/00list
+++ b/debian/patches/00list
@@ -1,4 +1,2 @@
-jessie_lib
 logopath
-makefile.in
 altergo
diff --git a/debian/patches/jessie_lib.dpatch b/debian/patches/jessie_lib.dpatch
deleted file mode 100755
index 6086879..0000000
--- a/debian/patches/jessie_lib.dpatch
+++ /dev/null
@@ -1,28 +0,0 @@
-#! /bin/sh /usr/share/dpatch/dpatch-run
-## jessie_lib.dpatch by  <dogguy at pps.jussieu.fr>
-##
-## DP: Make jc_ast.ml and jc_env.ml fit correctly in the pack
-
- at DPATCH@
-diff -urNad why~/Makefile.in why/Makefile.in
---- why~/Makefile.in	2009-08-27 20:11:39.000000000 +0200
-+++ why/Makefile.in	2009-08-27 20:35:12.000000000 +0200
-@@ -276,15 +276,15 @@
- 
- # jessie
- JCCML_EXPORT = src/lib.ml src/rc.ml src/loc.ml src/pp.ml src/option_misc.ml \
--	jc/jc_type_var.ml jc/output.ml \
-+	jc/jc_type_var.ml jc/jc_env.ml jc/output.ml \
- 	jc/jc_common_options.ml jc/jc_stdlib.ml \
--	jc/jc_envset.ml jc/jc_region.ml jc/jc_fenv.ml \
-+	jc/jc_envset.ml jc/jc_region.ml jc/jc_ast.ml jc/jc_fenv.ml \
- 	jc/jc_constructors.ml \
- 	jc/jc_pervasives.ml jc/jc_iterators.ml \
- 	jc/jc_output_misc.ml jc/jc_poutput.ml jc/jc_output.ml jc/jc_noutput.ml
- JCCMO_EXPORT = $(JCCML_EXPORT:.ml=.cmo)
- JCCMX_EXPORT = $(JCCML_EXPORT:.ml=.cmx)
--JCCMI_EXPORT = jc/jc_ast.cmi jc/jc_env.cmi $(JCCML_EXPORT:.ml=.cmi)
-+JCCMI_EXPORT = $(JCCML_EXPORT:.ml=.cmi)
- 
- JCCMO = src/version.cmo \
- 	@ATPCMO@ $(JCCMO_EXPORT) \
diff --git a/debian/patches/makefile.in.dpatch b/debian/patches/makefile.in.dpatch
deleted file mode 100755
index 097a1d9..0000000
--- a/debian/patches/makefile.in.dpatch
+++ /dev/null
@@ -1,17 +0,0 @@
-#! /bin/sh /usr/share/dpatch/dpatch-run
-## makefile.in.dpatch by  <dogguy at pps.jussieu.fr>
-##
-## DP: directory examples-v7 does not exist.
-
- at DPATCH@
-diff -urNad why~/Makefile.in why/Makefile.in
---- why~/Makefile.in	2008-11-08 21:07:42.000000000 +0100
-+++ why/Makefile.in	2008-11-08 21:08:08.000000000 +0100
-@@ -1112,7 +1112,6 @@
- 	rm -f $(GENERATED)
- 	make -C atp clean
- 	make -C doc clean
--	make -C examples-v7 clean
- 	make -C examples clean
- 
- dist-clean:: clean
diff --git a/debian/rules b/debian/rules
index 0eadedb..87dad0c 100755
--- a/debian/rules
+++ b/debian/rules
@@ -5,12 +5,10 @@ export DH_VERBOSE=1
 
 include /usr/share/dpatch/dpatch.make
 include /usr/share/ocaml/ocamlvars.mk
-include /usr/share/ocaml/ocamlinit.mk
 include /usr/share/coq/coqvars.mk
 
 WHYDIR    = $(CURDIR)/debian/why
 VERSION   = $(shell cat Version | grep ^VERSION | cut -d= -f 2)
-MLBACKUP  = jc/jc_ast jc/jc_env
 
 OCAMLINIT_SED += -e 's/@VERSION@/$(VERSION)/g'
 
@@ -24,6 +22,7 @@ endif
 
 config.status: configure
 	dh_testdir
+	dh_ocamlinit
 	./configure \
 	    --host=$(DEB_HOST_GNU_TYPE) \
 	    --build=$(DEB_BUILD_GNU_TYPE) \
@@ -33,26 +32,21 @@ config.status: configure
 	    --infodir=\$${prefix}/share/info CFLAGS="$(CFLAGS)" \
 	    LDFLAGS="-Wl,-z,defs"
 	cp .depend .depend.debian
-	for i in $(MLBACKUP); do \
-		mv $$i.mli $$i.ml; \
-	done
 
-build: ocamlinit patch-stamp build-stamp
+build: patch-stamp build-stamp
 build-stamp: config.status
 	dh_testdir
 	$(MAKE)
 	touch $@
 
-clean: unpatch ocamlinit-clean
+clean: unpatch
 	dh_testdir
 	dh_testroot
+	dh_ocamlinit -d
 	[ ! -f Makefile ] || sed -e 's/include .depend.*//g' Makefile > Makefile.debian
 	[ ! -f Makefile.debian ] || $(MAKE) -f Makefile.debian clean
 	-cp lib/coq/WhyCoq8.v lib/coq/WhyCoqCompat.v
 	[ ! -f .depend.debian ]  || mv .depend.debian .depend
-	for i in $(MLBACKUP); do \
-		[ ! -f $$i.ml ] || mv $$i.ml $$i.mli; \
-	done
 	$(RM) -f lib/coq/*.glob
 	dh_clean
 
@@ -66,11 +60,7 @@ install: build
 		COQLIB=$(CURDIR)/debian/libwhy-coq/$(COQ_STDLIB_DIR)
 	#Used to remove /usr/share/coq/jessie_why.v which is alone and installed by libwhy-coq
 	-$(RM) -rf $(WHYDIR)/usr/share/coq/
-	echo 'F:OCamlRuntime=$(OCAML_RUNTIME_NOX)' >> debian/libjessie-ocaml-dev.substvars
 	echo 'F:CoqABI=$(COQ_ABI)' >> debian/libwhy-coq.substvars
-ifeq ($(OCAML_OPT_ARCH),)
-	echo 'F:WhyRuntime=liblablgtk2-ocaml,$(OCAML_RUNTIME_NOX)' >> debian/why.substvars
-endif
 
 # Build architecture-independent files here.
 binary-indep: build install
@@ -90,6 +80,7 @@ binary-arch: build install
 	dh_fixperms
 	dh_installdeb
 	dh_shlibdeps
+	dh_ocaml
 	dh_gencontrol -- -VF:OCamlABI="$(OCAML_ABI)"
 	dh_md5sums
 	dh_builddeb

-- 
why packaging

