--- coq-float-8.1-1.0.orig/debian/changelog +++ coq-float-8.1-1.0/debian/changelog @@ -0,0 +1,20 @@ +coq-float (1:8.1-1.0-2) unstable; urgency=low + + * Rebuild with latest version of coq. + + -- Samuel Mimram Mon, 10 Sep 2007 00:24:19 +0200 + +coq-float (1:8.1-1.0-1) unstable; urgency=low + + * New upstream release. + * Updated upstream url and watch. + * Made the package arch all since coq libraries should be + platform-independant. + + -- Samuel Mimram Thu, 30 Aug 2007 13:08:49 +0200 + +coq-float (2001-1) unstable; urgency=low + + * Initial release, closes: #438613. + + -- Samuel Mimram Fri, 10 Aug 2007 14:48:56 +0000 --- coq-float-8.1-1.0.orig/debian/control +++ coq-float-8.1-1.0/debian/control @@ -0,0 +1,12 @@ +Source: coq-float +Section: libdevel +Priority: optional +Maintainer: Samuel Mimram +Build-Depends: debhelper (>= 5), coq (>= 8.1.pl1+dfsg-3) +Standards-Version: 3.7.2 + +Package: libfloat-coq +Architecture: all +Depends: ${shlibs:Depends}, coq (>= 8.1) +Description: coq library for floating point numbers + Library for reasoning about floating point numbers in coq. --- coq-float-8.1-1.0.orig/debian/dirs +++ coq-float-8.1-1.0/debian/dirs @@ -0,0 +1,2 @@ +usr/lib/coq/user-contrib +usr/share/doc/libfloat-coq/html --- coq-float-8.1-1.0.orig/debian/compat +++ coq-float-8.1-1.0/debian/compat @@ -0,0 +1 @@ +5 --- coq-float-8.1-1.0.orig/debian/watch +++ coq-float-8.1-1.0/debian/watch @@ -0,0 +1,3 @@ +version=3 + +http://lipforge.ens-lyon.fr/frs/?group_id=11&release_id=85 .*/Float([0-9a-z\-\.]*)\.tar\.gz --- coq-float-8.1-1.0.orig/debian/svn-deblayout +++ coq-float-8.1-1.0/debian/svn-deblayout @@ -0,0 +1,3 @@ +origDir=../upstream +origUrl=svn+ssh://svn.debian.org/svn/pkg-ocaml-maint/trunk/packages/coq-float/upstream +tagsUrl=svn+ssh://svn.debian.org/svn/pkg-ocaml-maint/tags/packages/coq-float --- coq-float-8.1-1.0.orig/debian/copyright +++ coq-float-8.1-1.0/debian/copyright @@ -0,0 +1,34 @@ +This package was debianized by Samuel Mimram on +Fri, 10 Aug 2007 14:48:56 +0000. + +It was downloaded from http://lipforge.ens-lyon.fr/www/pff/ + +Upstream Authors: Laurent Théry + Sylvie Boldo + Laurence Rideau + Laurent Fousse + +Copyright (C) 2001 Laurent Théry, Sylvie Boldo, Laurence Rideau and Laurent Fousse. + +License: + + This package is free software; you can redistribute it and/or + modify it under the terms of the GNU Lesser General Public + License as published by the Free Software Foundation; either + version 2 of the License, or (at your option) any later version. + + This package is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU + Lesser General Public License for more details. + + You should have received a copy of the GNU Lesser General Public + License along with this package; if not, write to the Free Software + Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA + +On Debian systems, the complete text of the GNU Lesser General +Public License can be found in `/usr/share/common-licenses/LGPL'. + + +The Debian packaging is (C) 2007, Samuel Mimram and +is licensed under the GPL, see `/usr/share/common-licenses/GPL'. --- coq-float-8.1-1.0.orig/debian/rules +++ coq-float-8.1-1.0/debian/rules @@ -0,0 +1,72 @@ +#!/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 + +DESTDIR := debian/libfloat-coq/$(shell coqc -where)/user-contrib + +INCDIRS := $(shell find . -type d) +INCDIRS := $(INCDIRS:%=-I %) + +configure: configure-stamp +configure-stamp: + dh_testdir + touch configure-stamp + + +build: build-stamp +build-stamp: configure-stamp + dh_testdir + + coq_makefile $(INCDIRS) $(shell find . -name \*.v) > Makefile + $(MAKE) depend + $(MAKE) all + $(MAKE) html + + touch $@ + +clean: + dh_testdir + dh_testroot + rm -f build-stamp configure-stamp + + [ ! -f Makefile ] || $(MAKE) clean + + dh_clean + +install: build + dh_testdir + dh_testroot + dh_clean -k + dh_installdirs + + cp $(shell find . -name \*.vo) $(DESTDIR) + cp $(wildcard *.html) debian/libfloat-coq/usr/share/doc/libfloat-coq/html + +binary-indep: build install + +binary-arch: build install + dh_testdir + dh_testroot + dh_installchangelogs + dh_installdocs + dh_installexamples + dh_installman + dh_link + dh_strip + dh_compress + dh_fixperms + dh_installdeb + dh_shlibdeps + dh_gencontrol + dh_md5sums + dh_builddeb + +binary: binary-indep binary-arch +.PHONY: build clean binary-indep binary-arch binary install configure --- coq-float-8.1-1.0.orig/.depend +++ coq-float-8.1-1.0/.depend @@ -0,0 +1,204 @@ +AllFloat.vo: AllFloat.v ClosestMult.vo Closest2Plus.vo +AllFloat.vi: AllFloat.v ClosestMult.vo Closest2Plus.vo +Closest2Plus.vo: Closest2Plus.v ClosestPlus.vo Closest2Prop.vo +Closest2Plus.vi: Closest2Plus.v ClosestPlus.vo Closest2Prop.vo +Closest2Prop.vo: Closest2Prop.v ClosestProp.vo +Closest2Prop.vi: Closest2Prop.v ClosestProp.vo +ClosestMult.vo: ClosestMult.v FroundMult.vo ClosestProp.vo +ClosestMult.vi: ClosestMult.v FroundMult.vo ClosestProp.vo +ClosestPlus.vo: ClosestPlus.v FroundPlus.vo ClosestProp.vo +ClosestPlus.vi: ClosestPlus.v FroundPlus.vo ClosestProp.vo +ClosestProp.vo: ClosestProp.v FroundProp.vo Closest.vo +ClosestProp.vi: ClosestProp.v FroundProp.vo Closest.vo +Closest.vo: Closest.v Fround.vo +Closest.vi: Closest.v Fround.vo +Digit.vo: Digit.v Faux.vo +Digit.vi: Digit.v Faux.vo +Faux.vo: Faux.v sTactic.vo +Faux.vi: Faux.v sTactic.vo +Fbound.vo: Fbound.v Fop.vo +Fbound.vi: Fbound.v Fop.vo +Fcomp.vo: Fcomp.v Float.vo +Fcomp.vi: Fcomp.v Float.vo +Finduct.vo: Finduct.v FPred.vo +Finduct.vi: Finduct.v FPred.vo +Float.vo: Float.v Rpow.vo +Float.vi: Float.v Rpow.vo +Fmin.vo: Fmin.v Zenum.vo FPred.vo +Fmin.vi: Fmin.v Zenum.vo FPred.vo +Fnorm.vo: Fnorm.v Fbound.vo +Fnorm.vi: Fnorm.v Fbound.vo +Fodd.vo: Fodd.v Fmin.vo +Fodd.vi: Fodd.v Fmin.vo +Fop.vo: Fop.v Fcomp.vo +Fop.vi: Fop.v Fcomp.vo +FPred.vo: FPred.v FSucc.vo +FPred.vi: FPred.v FSucc.vo +Fprop.vo: Fprop.v Fbound.vo +Fprop.vi: Fprop.v Fbound.vo +FroundMult.vo: FroundMult.v FroundProp.vo +FroundMult.vi: FroundMult.v FroundProp.vo +FroundPlus.vo: FroundPlus.v Finduct.vo FroundProp.vo +FroundPlus.vi: FroundPlus.v Finduct.vo FroundProp.vo +FroundProp.vo: FroundProp.v Fround.vo MSB.vo +FroundProp.vi: FroundProp.v Fround.vo MSB.vo +Fround.vo: Fround.v Fprop.vo Fodd.vo +Fround.vi: Fround.v Fprop.vo Fodd.vo +FSucc.vo: FSucc.v Fnorm.vo +FSucc.vi: FSucc.v Fnorm.vo +MSBProp.vo: MSBProp.v MSB.vo +MSBProp.vi: MSBProp.v MSB.vo +MSB.vo: MSB.v Fprop.vo Zdivides.vo Fnorm.vo +MSB.vi: MSB.v Fprop.vo Zdivides.vo Fnorm.vo +Option.vo: Option.v +Option.vi: Option.v +Paux.vo: Paux.v Digit.vo Option.vo +Paux.vi: Paux.v Digit.vo Option.vo +Rpow.vo: Rpow.v Digit.vo +Rpow.vi: Rpow.v Digit.vo +sTactic.vo: sTactic.v +sTactic.vi: sTactic.v +Zdivides.vo: Zdivides.v Paux.vo +Zdivides.vi: Zdivides.v Paux.vo +Zenum.vo: Zenum.v Faux.vo +Zenum.vi: Zenum.v Faux.vo +Ct2/FboundI.vo: Ct2/FboundI.v AllFloat.vo +Ct2/FboundI.vi: Ct2/FboundI.v AllFloat.vo +Ct2/FnormI.vo: Ct2/FnormI.v Ct2/FboundI.vo +Ct2/FnormI.vi: Ct2/FnormI.v Ct2/FboundI.vo +Expansions/EFast2Sum.vo: Expansions/EFast2Sum.v Expansions/Fast2Sum.vo +Expansions/EFast2Sum.vi: Expansions/EFast2Sum.v Expansions/Fast2Sum.vo +Expansions/Fast2Diff.vo: Expansions/Fast2Diff.v Expansions/EFast2Sum.vo +Expansions/Fast2Diff.vi: Expansions/Fast2Diff.v Expansions/EFast2Sum.vo +Expansions/Fast2Sum.vo: Expansions/Fast2Sum.v AllFloat.vo +Expansions/Fast2Sum.vi: Expansions/Fast2Sum.v AllFloat.vo +Expansions/Fexp2.vo: Expansions/Fexp2.v Expansions/ThreeSumProps.vo +Expansions/Fexp2.vi: Expansions/Fexp2.v Expansions/ThreeSumProps.vo +Expansions/FexpAdd.vo: Expansions/FexpAdd.v Expansions/Fexp2.vo +Expansions/FexpAdd.vi: Expansions/FexpAdd.v Expansions/Fexp2.vo +Expansions/FexpDiv.vo: Expansions/FexpDiv.v AllFloat.vo +Expansions/FexpDiv.vi: Expansions/FexpDiv.v AllFloat.vo +Expansions/FexpPlus.vo: Expansions/FexpPlus.v Expansions/Fexp.vo +Expansions/FexpPlus.vi: Expansions/FexpPlus.v Expansions/Fexp.vo +Expansions/Fexp.vo: Expansions/Fexp.v AllFloat.vo +Expansions/Fexp.vi: Expansions/Fexp.v AllFloat.vo +Expansions/ThreeSum2.vo: Expansions/ThreeSum2.v AllFloat.vo +Expansions/ThreeSum2.vi: Expansions/ThreeSum2.v AllFloat.vo +Expansions/ThreeSumProps.vo: Expansions/ThreeSumProps.v Expansions/ThreeSum2.vo +Expansions/ThreeSumProps.vi: Expansions/ThreeSumProps.v Expansions/ThreeSum2.vo +Expansions/TwoSum.vo: Expansions/TwoSum.v Expansions/Fast2Sum.vo +Expansions/TwoSum.vi: Expansions/TwoSum.v Expansions/Fast2Sum.vo +FnElem/Axpy.vo: FnElem/Axpy.v FnElem/MinOrMax.vo +FnElem/Axpy.vi: FnElem/Axpy.v FnElem/MinOrMax.vo +FnElem/DoubleRound.vo: FnElem/DoubleRound.v FnElem/MinOrMax.vo +FnElem/DoubleRound.vi: FnElem/DoubleRound.v FnElem/MinOrMax.vo +FnElem/FArgReduct2.vo: FnElem/FArgReduct2.v FnElem/FArgReduct.vo +FnElem/FArgReduct2.vi: FnElem/FArgReduct2.v FnElem/FArgReduct.vo +FnElem/FArgReduct3.vo: FnElem/FArgReduct3.v FnElem/FArgReduct2.vo +FnElem/FArgReduct3.vi: FnElem/FArgReduct3.v FnElem/FArgReduct2.vo +FnElem/FArgReduct4.vo: FnElem/FArgReduct4.v Others/Dekker.vo Others/discriminant3.vo FnElem/FmaErr.vo FnElem/FArgReduct3.vo +FnElem/FArgReduct4.vi: FnElem/FArgReduct4.v Others/Dekker.vo Others/discriminant3.vo FnElem/FmaErr.vo FnElem/FArgReduct3.vo +FnElem/FArgReduct.vo: FnElem/FArgReduct.v Ct2/FnormI.vo +FnElem/FArgReduct.vi: FnElem/FArgReduct.v Ct2/FnormI.vo +FnElem/FIA64elem.vo: FnElem/FIA64elem.v AllFloat.vo +FnElem/FIA64elem.vi: FnElem/FIA64elem.v AllFloat.vo +FnElem/FmaErrApprox.vo: FnElem/FmaErrApprox.v AllFloat.vo Others/Veltkamp.vo FnElem/FmaErr.vo +FnElem/FmaErrApprox.vi: FnElem/FmaErrApprox.v AllFloat.vo Others/Veltkamp.vo FnElem/FmaErr.vo +FnElem/FmaErr.vo: FnElem/FmaErr.v AllFloat.vo Others/Veltkamp.vo +FnElem/FmaErr.vi: FnElem/FmaErr.v AllFloat.vo Others/Veltkamp.vo +FnElem/MinOrMax.vo: FnElem/MinOrMax.v AllFloat.vo +FnElem/MinOrMax.vi: FnElem/MinOrMax.v AllFloat.vo +Others/DblRndOdd.vo: Others/DblRndOdd.v AllFloat.vo +Others/DblRndOdd.vi: Others/DblRndOdd.v AllFloat.vo +Others/Dekker.vo: Others/Dekker.v Others/Veltkamp.vo +Others/Dekker.vi: Others/Dekker.v Others/Veltkamp.vo +Others/discriminant2.vo: Others/discriminant2.v AllFloat.vo +Others/discriminant2.vi: Others/discriminant2.v AllFloat.vo +Others/discriminant3.vo: Others/discriminant3.v Others/discriminant2.vo +Others/discriminant3.vi: Others/discriminant3.v Others/discriminant2.vo +Others/discriminant.vo: Others/discriminant.v AllFloat.vo +Others/discriminant.vi: Others/discriminant.v AllFloat.vo +Others/Divnk.vo: Others/Divnk.v AllFloat.vo +Others/Divnk.vi: Others/Divnk.v AllFloat.vo +Others/FmaEmul.vo: Others/FmaEmul.v Others/DblRndOdd.vo Ct2/FboundI.vo FnElem/MinOrMax.vo FnElem/DoubleRound.vo +Others/FmaEmul.vi: Others/FmaEmul.v Others/DblRndOdd.vo Ct2/FboundI.vo FnElem/MinOrMax.vo FnElem/DoubleRound.vo +Others/FminOp.vo: Others/FminOp.v AllFloat.vo Paux.vo +Others/FminOp.vi: Others/FminOp.v AllFloat.vo Paux.vo +Others/FroundDivSqrt.vo: Others/FroundDivSqrt.v AllFloat.vo +Others/FroundDivSqrt.vi: Others/FroundDivSqrt.v AllFloat.vo +Others/IEEE.vo: Others/IEEE.v AllFloat.vo +Others/IEEE.vi: Others/IEEE.v AllFloat.vo +Others/PradixE.vo: Others/PradixE.v FroundPlus.vo +Others/PradixE.vi: Others/PradixE.v FroundPlus.vo +Others/RND.vo: Others/RND.v AllFloat.vo +Others/RND.vi: Others/RND.v AllFloat.vo +Others/Veltkamp.vo: Others/Veltkamp.v AllFloat.vo +Others/Veltkamp.vi: Others/Veltkamp.v AllFloat.vo +AllFloat.html: AllFloat.v ClosestMult.html Closest2Plus.html +Closest2Plus.html: Closest2Plus.v ClosestPlus.html Closest2Prop.html +Closest2Prop.html: Closest2Prop.v ClosestProp.html +ClosestMult.html: ClosestMult.v FroundMult.html ClosestProp.html +ClosestPlus.html: ClosestPlus.v FroundPlus.html ClosestProp.html +ClosestProp.html: ClosestProp.v FroundProp.html Closest.html +Closest.html: Closest.v Fround.html +Digit.html: Digit.v Faux.html +Faux.html: Faux.v sTactic.html +Fbound.html: Fbound.v Fop.html +Fcomp.html: Fcomp.v Float.html +Finduct.html: Finduct.v FPred.html +Float.html: Float.v Rpow.html +Fmin.html: Fmin.v Zenum.html FPred.html +Fnorm.html: Fnorm.v Fbound.html +Fodd.html: Fodd.v Fmin.html +Fop.html: Fop.v Fcomp.html +FPred.html: FPred.v FSucc.html +Fprop.html: Fprop.v Fbound.html +FroundMult.html: FroundMult.v FroundProp.html +FroundPlus.html: FroundPlus.v Finduct.html FroundProp.html +FroundProp.html: FroundProp.v Fround.html MSB.html +Fround.html: Fround.v Fprop.html Fodd.html +FSucc.html: FSucc.v Fnorm.html +MSBProp.html: MSBProp.v MSB.html +MSB.html: MSB.v Fprop.html Zdivides.html Fnorm.html +Option.html: Option.v +Paux.html: Paux.v Digit.html Option.html +Rpow.html: Rpow.v Digit.html +sTactic.html: sTactic.v +Zdivides.html: Zdivides.v Paux.html +Zenum.html: Zenum.v Faux.html +Ct2/FboundI.html: Ct2/FboundI.v AllFloat.html +Ct2/FnormI.html: Ct2/FnormI.v Ct2/FboundI.html +Expansions/EFast2Sum.html: Expansions/EFast2Sum.v Expansions/Fast2Sum.html +Expansions/Fast2Diff.html: Expansions/Fast2Diff.v Expansions/EFast2Sum.html +Expansions/Fast2Sum.html: Expansions/Fast2Sum.v AllFloat.html +Expansions/Fexp2.html: Expansions/Fexp2.v Expansions/ThreeSumProps.html +Expansions/FexpAdd.html: Expansions/FexpAdd.v Expansions/Fexp2.html +Expansions/FexpDiv.html: Expansions/FexpDiv.v AllFloat.html +Expansions/FexpPlus.html: Expansions/FexpPlus.v Expansions/Fexp.html +Expansions/Fexp.html: Expansions/Fexp.v AllFloat.html +Expansions/ThreeSum2.html: Expansions/ThreeSum2.v AllFloat.html +Expansions/ThreeSumProps.html: Expansions/ThreeSumProps.v Expansions/ThreeSum2.html +Expansions/TwoSum.html: Expansions/TwoSum.v Expansions/Fast2Sum.html +FnElem/Axpy.html: FnElem/Axpy.v FnElem/MinOrMax.html +FnElem/DoubleRound.html: FnElem/DoubleRound.v FnElem/MinOrMax.html +FnElem/FArgReduct2.html: FnElem/FArgReduct2.v FnElem/FArgReduct.html +FnElem/FArgReduct3.html: FnElem/FArgReduct3.v FnElem/FArgReduct2.html +FnElem/FArgReduct4.html: FnElem/FArgReduct4.v Others/Dekker.html Others/discriminant3.html FnElem/FmaErr.html FnElem/FArgReduct3.html +FnElem/FArgReduct.html: FnElem/FArgReduct.v Ct2/FnormI.html +FnElem/FIA64elem.html: FnElem/FIA64elem.v AllFloat.html +FnElem/FmaErrApprox.html: FnElem/FmaErrApprox.v AllFloat.html Others/Veltkamp.html FnElem/FmaErr.html +FnElem/FmaErr.html: FnElem/FmaErr.v AllFloat.html Others/Veltkamp.html +FnElem/MinOrMax.html: FnElem/MinOrMax.v AllFloat.html +Others/DblRndOdd.html: Others/DblRndOdd.v AllFloat.html +Others/Dekker.html: Others/Dekker.v Others/Veltkamp.html +Others/discriminant2.html: Others/discriminant2.v AllFloat.html +Others/discriminant3.html: Others/discriminant3.v Others/discriminant2.html +Others/discriminant.html: Others/discriminant.v AllFloat.html +Others/Divnk.html: Others/Divnk.v AllFloat.html +Others/FmaEmul.html: Others/FmaEmul.v Others/DblRndOdd.html Ct2/FboundI.html FnElem/MinOrMax.html FnElem/DoubleRound.html +Others/FminOp.html: Others/FminOp.v AllFloat.html Paux.html +Others/FroundDivSqrt.html: Others/FroundDivSqrt.v AllFloat.html +Others/IEEE.html: Others/IEEE.v AllFloat.html +Others/PradixE.html: Others/PradixE.v FroundPlus.html +Others/RND.html: Others/RND.v AllFloat.html +Others/Veltkamp.html: Others/Veltkamp.v AllFloat.html