[Pkg-ocaml-maint-commits] [SCM] alt-ergo packaging branch, master, updated. upstream/0.8-1-g0b16f44

Mehdi Dogguy dogguy at pps.jussieu.fr
Wed Nov 5 21:05:50 UTC 2008 

The following commit has been merged in the master branch:
commit 0b16f441530dadf610c886b080e0a870a703a1b2
Author: Mehdi Dogguy <dogguy at pps.jussieu.fr>
Date:   Wed Nov 5 21:56:47 2008 +0100

    Initial import of the debian directory

diff --git a/debian/alt-ergo.dirs b/debian/alt-ergo.dirs
new file mode 100644
index 0000000..1acef58
--- /dev/null
+++ b/debian/alt-ergo.dirs
@@ -0,0 +1,3 @@
+usr/bin
+usr/lib/alt-ergo
+
diff --git a/debian/alt-ergo.manpages b/debian/alt-ergo.manpages
new file mode 100644
index 0000000..c600eea
--- /dev/null
+++ b/debian/alt-ergo.manpages
@@ -0,0 +1 @@
+doc/alt-ergo.1
diff --git a/debian/changelog b/debian/changelog
new file mode 100644
index 0000000..e78171b
--- /dev/null
+++ b/debian/changelog
@@ -0,0 +1,5 @@
+alt-ergo (0.8-1) UNRELEASED; urgency=low
+
+  * Initial release (Closes: #468557)
+
+ -- Mehdi Dogguy <dogguy at pps.jussieu.fr>  Wed, 10 Sep 2008 10:13:00 +0100
diff --git a/debian/compat b/debian/compat
new file mode 100644
index 0000000..1e8b314
--- /dev/null
+++ b/debian/compat
@@ -0,0 +1 @@
+6
diff --git a/debian/control b/debian/control
new file mode 100644
index 0000000..c5c7dd9
--- /dev/null
+++ b/debian/control
@@ -0,0 +1,24 @@
+Source: alt-ergo
+Section: math
+Priority: optional
+Maintainer: Debian OCaml Maintainers <debian-ocaml-maint at lists.debian.org>
+Uploaders: Mehdi Dogguy <dogguy at pps.jussieu.fr>
+Build-Depends: debhelper (>= 6), autotools-dev, ocaml-nox (>= 3.10.0), libocamlgraph-ocaml-dev, dpatch
+Homepage: http://alt-ergo.lri.fr
+Standards-Version: 3.8.0
+Vcs-Svn: svn://svn.debian.org/svn/pkg-ocaml-maint/trunk/packages/ergo
+Vcs-Browser: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/ergo/trunk/
+
+Package: alt-ergo
+Architecture: any
+Depends: ${shlibs:Depends}, ${misc:Depends}, ${F:OCamlRun}
+Suggests: why
+Description: Automatic theorem prover dedicated to program verification
+ Alt-Ergo is an automatic theorem prover dedicated to program verification. 
+ Alt-Ergo is based on CC(X) a congruence closure algorithm parameterized by an 
+ equational theory X. Currently, CC(X) can be instantiated by the empty 
+ equational theory and by the linear arithmetics. Alt-Ergo contains also a home 
+ made SAT-solver and an instantiation mechanism.
+ .
+ Alt-Ergo is both safe and modular: each box is described by a small set of 
+ inference rules and is implemented as an OCaml functor.
diff --git a/CeCILL-C b/debian/copyright
similarity index 95%
copy from CeCILL-C
copy to debian/copyright
index 3d2a819..701557e 100644
--- a/CeCILL-C
+++ b/debian/copyright
@@ -1,5 +1,28 @@
+This package was debianized by Mehdi Dogguy <dogguy at pps.jussieu.fr> on
+Fri, 22 Feb 2008 10:09:03 +0100.
 
-CeCILL-C FREE SOFTWARE LICENSE AGREEMENT
+It was downloaded from <http://alt-ergo.lri.fr/http/>
+
+Files: heap.ml{,i}
+Copyright: © 2003 Jean-Christophe FILLIÂTRE <filliatr at lri.fr>
+           © 1996 INRIA
+
+Files: configure.in,Makefile.in
+Copyright: © 2001 Jean-Christophe FILLIÂTRE <filliatr at lri.fr>
+
+Files: hashcons.ml{,i}
+Copyright: © 2000 Jean-Christophe FILLIÂTRE <filliatr at lri.fr>
+
+Files: why_lexer.mll,why_parser.mly
+Copyright: © 2002 Jean-Christophe FILLIÂTRE <filliatr at lri.fr>
+
+Copyright: © 2006 Sylvain Conchon
+License: CeCILL-C
+
+    Alt-Ergo's licence is CeCILL-C:
+
+
+                 CeCILL-C FREE SOFTWARE LICENSE AGREEMENT
 
 
     Notice
@@ -19,7 +42,7 @@ the two main principles guiding its drafting:
 The authors of the CeCILL-C (for Ce[a] C[nrs] I[nria] L[ogiciel] L[ibre])
 license are:
 
-Commissariat à l'Energie Atomique - CEA, a public scientific, technical
+Commissariat à l'Energie Atomique - CEA, a public scientific, technical
 and industrial research establishment, having its principal place of
 business at 25 rue Leblanc, immeuble Le Ponant D, 75015 Paris, France.
 
@@ -338,7 +361,7 @@ The Licensee expressly undertakes:
 
 The Licensee undertakes not to directly or indirectly infringe the
 intellectual property rights of the Holder and/or Contributors on the
-Software and to take, where applicable, vis-à-vis its staff, any and all
+Software and to take, where applicable, vis-à-vis its staff, any and all
 measures required to ensure respect of said intellectual property rights
 of the Holder and/or Contributors.
 
@@ -515,3 +538,7 @@ jurisdiction, by the more diligent Party.
 
 
 Version 1.0 dated 2006-09-05.
+
+
+The Debian packaging is © 2008, Mehdi Dogguy <dogguy at pps.jussieu.fr> and
+is licensed under the GPL, see `/usr/share/common-licenses/GPL'.
diff --git a/debian/docs b/debian/docs
new file mode 100644
index 0000000..e845566
--- /dev/null
+++ b/debian/docs
@@ -0,0 +1 @@
+README
diff --git a/debian/patches/00list b/debian/patches/00list
new file mode 100644
index 0000000..2851015
--- /dev/null
+++ b/debian/patches/00list
@@ -0,0 +1 @@
+01_no_debug
diff --git a/debian/patches/01_no_debug.dpatch b/debian/patches/01_no_debug.dpatch
new file mode 100755
index 0000000..303dba6
--- /dev/null
+++ b/debian/patches/01_no_debug.dpatch
@@ -0,0 +1,18 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## 02_better_Makefile.dpatch by  <dogguy at pps.jussieu.fr>
+##
+## DP: Removes debug flag from bytecode executable.
+
+ at DPATCH@
+diff -urNad trunk~/Makefile.in trunk/Makefile.in
+--- trunk~/Makefile.in	2008-07-21 22:05:29.000000000 +0200
++++ trunk/Makefile.in	2008-09-10 10:10:29.000000000 +0200
+@@ -41,7 +41,7 @@
+ EXE = @EXE@
+ 
+ INCLUDES = @OCAMLGRAPHLIB@ 
+-BFLAGS = -dtypes -g $(INCLUDES)
++BFLAGS = -dtypes $(INCLUDES)
+ OFLAGS = -dtypes $(INCLUDES)
+ 
+ BIBBYTE=nums.cma graph.cma unix.cma
diff --git a/debian/rules b/debian/rules
new file mode 100755
index 0000000..670b0b9
--- /dev/null
+++ b/debian/rules
@@ -0,0 +1,81 @@
+#!/usr/bin/make -f
+# -*- makefile -*-
+# Sample debian/rules that uses debhelper.
+# This file was originally written by Joey Hess and Craig Small.
+# As a special exception, when this file is copied by dh-make into a
+# dh-make output file, you may use that output file without restriction.
+# This special exception was added by Craig Small in version 0.37 of dh-make.
+
+# Uncomment this to turn on verbose mode.
+#export DH_VERBOSE=1
+
+include /usr/share/dpatch/dpatch.make
+
+DEB_HOST_GNU_TYPE  ?= $(shell dpkg-architecture -qDEB_HOST_GNU_TYPE)
+DEB_BUILD_GNU_TYPE ?= $(shell dpkg-architecture -qDEB_BUILD_GNU_TYPE)
+
+OCAMLABI  = $(shell ocamlc -version)
+BYTECODE  = $(shell [ -x /usr/bin/ocamlopt ] || echo yes)
+OCAMLRUN  = $(if $(BYTECODE),ocaml-base-nox-$(OCAMLABI),)
+OCAMLBEST = $(if $(BYTECODE),byte,opt)
+MAKEOPTS  = OCAMLC=ocamlc OCAMLOPT=ocamlopt OCAMLLEX=ocamllex OCAMLLIB=/usr/lib/ocaml/$(OCAMLABI) OCAMLVERSION=$(OCAMLABI)
+
+config.status: 
+	dh_testdir
+	./configure --host=$(DEB_HOST_GNU_TYPE) \
+	--build=$(DEB_BUILD_GNU_TYPE)           \
+	--prefix=/usr                           \
+	--mandir=\$${prefix}/share/man
+
+build: patch build-arch
+
+build-indep: build-indep-stamp
+build-indep-stamp:
+	touch $@
+
+build-arch: build-arch-stamp
+build-arch-stamp: config.status
+	dh_testdir
+	$(MAKE) $(OCAMLBEST)
+	touch $@
+
+clean: unpatch
+	dh_testdir
+	dh_testroot
+	rm -f build-stamp build-indep-stamp build-arch-stamp
+	if [ -f Makefile ]; then \
+		$(MAKE) clean;   \
+	fi
+	dh_clean 
+	-rm -f config.status Makefile
+
+install: build
+	dh_testdir
+	dh_testroot
+	dh_clean -k 
+	dh_installdirs
+	cp -f alt-ergo.$(OCAMLBEST) $(CURDIR)/debian/alt-ergo/usr/bin/alt-ergo
+	cp -f smt_prelude.mlw $(CURDIR)/debian/alt-ergo/usr/lib/alt-ergo/
+
+binary-indep: build install
+
+binary-arch: build install
+	dh_testdir
+	dh_testroot
+	dh_installchangelogs CHANGES
+	dh_installdocs
+	dh_installman
+	dh_link
+	if [ "$(OCAMLBEST)" = "opt" ]; then \
+		dh_strip;                   \
+	fi
+	dh_compress
+	dh_fixperms
+	dh_installdeb
+	dh_shlibdeps
+	dh_gencontrol -- -VF:OCamlRun="$(OCAMLRUN)"
+	dh_md5sums
+	dh_builddeb
+
+binary: binary-indep binary-arch
+.PHONY: build clean binary-indep binary-arch binary install 
diff --git a/debian/watch b/debian/watch
new file mode 100644
index 0000000..e5463c6
--- /dev/null
+++ b/debian/watch
@@ -0,0 +1,3 @@
+version=3
+http://alt-ergo.lri.fr/http/alt-ergo-(.*)\.tar\.gz
+

-- 
alt-ergo packaging

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