--- agda-2.2.6.orig/debian/compat +++ agda-2.2.6/debian/compat @@ -0,0 +1 @@ +7 --- agda-2.2.6.orig/debian/control +++ agda-2.2.6/debian/control @@ -0,0 +1,160 @@ +Source: agda +Priority: extra +Section: haskell +Maintainer: Debian Haskell Group +Uploaders: Iain Lane +Build-Depends: debhelper (>= 7.0), + haskell-devscripts (>= 0.6.15+nmu12~), + cdbs (>> 0.4.58), + ghc6 (>= 6.10.3-2~), + ghc6-prof (>= 6.10.3-2~), + libghc6-quickcheck2-dev (>= 2.1.0.2), + libghc6-quickcheck2-dev (<< 2.2.0.0), + libghc6-binary-dev (>= 0.4.4), + libghc6-binary-dev (<< 0.6), + libghc6-haskeline-dev (>= 0.3), + libghc6-haskeline-dev (<< 0.7), + libghc6-haskell-src-dev (>= 1.0.1.1), + libghc6-haskell-src-dev (<< 2), + libghc6-mtl-dev (>= 1.1), + libghc6-mtl-dev (<< 2), + libghc6-utf8-string-dev (>= 0.3), + libghc6-utf8-string-dev (<< 0.4), + libghc6-xhtml-dev (>= 3000.2), + libghc6-xhtml-dev (<< 3000.3), + libghc6-zlib-dev (>= 0.4.0.1), + libghc6-zlib-dev (<< 1), + libghc6-quickcheck2-prof (>= 2.1.0.2), + libghc6-quickcheck2-prof (<< 2.2.0.0), + libghc6-binary-prof (>= 0.4.4), + libghc6-binary-prof (<< 0.6), + libghc6-haskeline-prof (>= 0.3), + libghc6-haskeline-prof (<< 0.7), + libghc6-haskell-src-prof (>= 1.0.1.1), + libghc6-haskell-src-prof (<< 2), + libghc6-mtl-prof (>= 1.1), + libghc6-mtl-prof (<< 2), + libghc6-utf8-string-prof (>= 0.3), + libghc6-utf8-string-prof (<< 0.4), + libghc6-xhtml-prof (>= 3000.2), + libghc6-xhtml-prof (<< 3000.3), + libghc6-zlib-prof (>= 0.4.0.1), + libghc6-zlib-prof (<< 1), + happy (>= 1.15), + happy (<< 2), + alex (>= 2.0.1), + alex (<< 3), + hscolour (>= 1.8), + ghc6-doc (>= 6.10.3-2~), + haddock (>= 2.4.2), + libncurses5-dev, + libghc6-quickcheck2-doc (>= 2.1.0.2), + libghc6-quickcheck2-doc (<< 2.2.0.0), + libghc6-binary-doc (>= 0.4.4), + libghc6-binary-doc (<< 0.6), + libghc6-haskeline-doc (>= 0.3), + libghc6-haskeline-doc (<< 0.7), + libghc6-haskell-src-doc (>= 1.0.1.1), + libghc6-haskell-src-doc (<< 2), + libghc6-mtl-doc (>= 1.1), + libghc6-mtl-doc (<< 2), + libghc6-terminfo-doc, + libghc6-utf8-string-doc (>= 0.3), + libghc6-utf8-string-doc (<< 0.4), + libghc6-xhtml-doc (>= 3000.2), + libghc6-xhtml-doc (<< 3000.3), + haskell-zlib-doc (>= 0.4.0.1), + haskell-zlib-doc (<< 1) +Standards-Version: 3.8.3 +Vcs-Browser: http://git.debian.org/?p=pkg-haskell/agda.git;a=summary +Vcs-Git: git://git.debian.org/git/pkg-haskell/agda.git +Homepage: http://wiki.portal.chalmers.se/agda/ + +Package: libghc6-agda-dev +Architecture: any +Section: haskell +Depends: ${haskell:Depends}, + ${misc:Depends}, +Suggests: ${haskell:Suggests} +Description: a dependently typed functional programming language - development libraries + Agda is a dependently typed functional programming language: It has inductive + families, which are like Haskell's GADTs, but they can be indexed by values and + not just types. It also has parameterised modules, mixfix operators, Unicode + characters, and an interactive Emacs interface (the type checker can assist in + the development of your code). + . + Agda is also a proof assistant: It is an interactive system for writing and + checking proofs. Agda is based on intuitionistic type theory, a foundational + system for constructive mathematics developed by the Swedish logician Per + Martin-Löf. It has many similarities with other proof assistants based on + dependent types, such as Coq, Epigram and NuPRL. + . + This package contains the normal library files. + +Package: libghc6-agda-prof +Architecture: any +Section: haskell +Depends: ${haskell:Depends}, + ${misc:Depends}, +Description: a dependently typed functional programming language - profiling libraries + Agda is a dependently typed functional programming language: It has inductive + families, which are like Haskell's GADTs, but they can be indexed by values and + not just types. It also has parameterised modules, mixfix operators, Unicode + characters, and an interactive Emacs interface (the type checker can assist in + the development of your code). + . + Agda is also a proof assistant: It is an interactive system for writing and + checking proofs. Agda is based on intuitionistic type theory, a foundational + system for constructive mathematics developed by the Swedish logician Per + Martin-Löf. It has many similarities with other proof assistants based on + dependent types, such as Coq, Epigram and NuPRL. + . + This package contains the libraries compiled with profiling enabled. + +Package: haskell-agda-doc +Architecture: all +Section: doc +Depends: ${misc:Depends} +Recommends: ${haskell:Recommends} +Suggests: ${haskell:Suggests} +Description: a dependently typed functional programming language - documentation + Agda is a dependently typed functional programming language: It has inductive + families, which are like Haskell's GADTs, but they can be indexed by values and + not just types. It also has parameterised modules, mixfix operators, Unicode + characters, and an interactive Emacs interface (the type checker can assist in + the development of your code). + . + Agda is also a proof assistant: It is an interactive system for writing and + checking proofs. Agda is based on intuitionistic type theory, a foundational + system for constructive mathematics developed by the Swedish logician Per + Martin-Löf. It has many similarities with other proof assistants based on + dependent types, such as Coq, Epigram and NuPRL. + . + This package contains the documentation files. + +Package: agda-mode +Architecture: all +Section: misc +Depends: ${shlibs:Depends}, + ${haskell:Depends}, + ${misc:Depends}, + emacs | emacsen, + haskell-mode, + libghc6-agda-dev (>= ${source:Version}), + libghc6-agda-dev (<< ${source:Version}.1~) +Description: the emacs mode for Agda + Agda is a dependently typed functional programming language: It has inductive + families, which are like Haskell's GADTs, but they can be indexed by values and + not just types. It also has parameterised modules, mixfix operators, Unicode + characters, and an interactive Emacs interface (the type checker can assist in + the development of your code). + . + Agda is also a proof assistant: It is an interactive system for writing and + checking proofs. Agda is based on intuitionistic type theory, a foundational + system for constructive mathematics developed by the Swedish logician Per + Martin-Löf. It has many similarities with other proof assistants based on + dependent types, such as Coq, Epigram and NuPRL. + . + This package contains the emacs interactive development mode for Agda. This + mode is the preferred way to write Agda code, and offers features such as + iterative development, refinement, case analysis and so on. --- agda-2.2.6.orig/debian/libghc6-agda-dev.install +++ agda-2.2.6/debian/libghc6-agda-dev.install @@ -0,0 +1 @@ +debian/tmp-inst-ghc6/usr/share/libghc6-agda-dev/Agda.css usr/share/libghc6-agda-dev/ --- agda-2.2.6.orig/debian/agda-mode.install +++ agda-2.2.6/debian/agda-mode.install @@ -0,0 +1,2 @@ +debian/tmp-inst-ghc6/usr/share/libghc6-agda-dev/emacs-mode/* usr/share/emacs/site-lisp/agda +debian/50agda.el etc/emacs/site-start.d/ --- agda-2.2.6.orig/debian/changelog +++ agda-2.2.6/debian/changelog @@ -0,0 +1,48 @@ +agda (2.2.6-2) unstable; urgency=low + + * debian/control: Set priority to extra per archive overrides + * debian/copyright: Update upstream source to a more generic location + * debian/rules, debian/libghc6-agda-dev.install: Install Agda.css, needed + to generate HTML documentation. + + -- Iain Lane Sun, 10 Jan 2010 11:29:17 +0000 + +agda (2.2.6-1) unstable; urgency=low + + * New upstream release 2.2.6, for headlines please see: + http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-2-6 + * debian/control + + Bump standards-version to 3.8.3, no changes + + Fix Vcs-Git to point to correct URL + + Update build-depends for new upstream release + + Undo arch/indep split per current pkg-haskell practice + + Add Homepage field + * debian/copyright: Fix encoding to UTF-8 (thanks Lintian) + * debian/README.source: Remove, no repacking so not necessary any more + * debian/50agda.el: + + Only load file if it exists, prevents a non-intrusive emacs warning + where 50agda.el is left on system when package is removed. + (Closes: #559197). + + Do not load file on XEmacs — agda-mode is not compatible with XEmacs. + + -- Iain Lane Tue, 05 Jan 2010 23:43:20 +0000 + +agda (2.2.4+dfsg-1) unstable; urgency=low + + * New upstream release 2.2.4. + * Repacked to fix a couple of DFSG problems, see debian/README.source for + more information. + * debian/copyright: Update, add missing copyright holders. + * debian/control: Move ghc6-doc, haddock to Build-Depends. Move -doc + packages to build-depends-indep. + + -- Iain Lane Mon, 20 Jul 2009 19:49:41 +0100 + +agda (2.2.2-1) unstable; urgency=low + + * Initial packaging (Closes: #522924) + * With thanks to Marco Túlio Gontijo e Silva and Joachim Breitner for + their helpful comments + + -- Iain Lane Wed, 20 May 2009 16:08:07 +0100 + --- agda-2.2.6.orig/debian/watch +++ agda-2.2.6/debian/watch @@ -0,0 +1,3 @@ +version=3 +opts="dversionmangle=s/\+dfsg//" \ +http://hackage.haskell.org/cgi-bin/hackage-scripts/package/Agda /packages/archive/Agda/.*/Agda-([\d\.]*)\.tar\.gz --- agda-2.2.6.orig/debian/copyright +++ agda-2.2.6/debian/copyright @@ -0,0 +1,69 @@ +Format-Specification: http://wiki.debian.org/Proposals/CopyrightFormat?action=recall&rev=196 +Upstream-Name: Agda +Upstream-Maintainer: Ulf Norell +Upstream-Source: http://hackage.haskell.org/package/Agda + +Files: * +Copyright: 2005-2009, Ulf Norell, Catarina Coquand, Makoto Takeyama, + Nils Anders Danielsson, Andreas Abel, Karl Mehltretter, Marcin Benke +License: MIT + +Files: src/full/Agda/Utils/ReadP.hs +Copyright: Copyright 2002, The University of Glasgow +License: Other + +Files: debian/* +Copyright: 2009, Iain Lane , + Marco Túlio Gontijo e Silva +License: MIT + +License: MIT + Copyright (c) 2005-2009 Ulf Norell, Nils Anders Danielsson, Catarina + Coquand, Makoto Takeyama, Andreas Abel, Karl Mehltretter, Marcin + Benke. + + Permission is hereby granted, free of charge, to any person obtaining a copy + of this software and associated documentation files (the "Software"), to deal + in the Software without restriction, including without limitation the rights + to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + . + The above copyright notice and this permission notice shall be included in + all copies or substantial portions of the Software. + . + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. + +License: Other + Redistribution and use in source and binary forms, with or without + modification, are permitted provided that the following conditions are met: + . + - Redistributions of source code must retain the above copyright notice, + this list of conditions and the following disclaimer. + . + - Redistributions in binary form must reproduce the above copyright notice, + this list of conditions and the following disclaimer in the documentation + and/or other materials provided with the distribution. + . + - Neither name of the University nor the names of its contributors may be + used to endorse or promote products derived from this software without + specific prior written permission. + . + THIS SOFTWARE IS PROVIDED BY THE UNIVERSITY COURT OF THE UNIVERSITY OF + GLASGOW AND THE CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, + INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND + FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE + UNIVERSITY COURT OF THE UNIVERSITY OF GLASGOW OR THE CONTRIBUTORS BE LIABLE + FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY + OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH + DAMAGE. --- agda-2.2.6.orig/debian/rules +++ agda-2.2.6/debian/rules @@ -0,0 +1,7 @@ +#!/usr/bin/make -f +DEB_BUILD_DEPENDENCIES = build-arch + +DEB_SETUP_GHC6_CONFIGURE_ARGS := --datadir='/usr/share' --datasubdir='libghc6-agda-dev' + +include /usr/share/cdbs/1/rules/debhelper.mk +include /usr/share/cdbs/1/class/hlibrary.mk --- agda-2.2.6.orig/debian/50agda.el +++ agda-2.2.6/debian/50agda.el @@ -0,0 +1,5 @@ +;; This conffile is left around if the package is removed but not purged. +;; agda-mode is also not compatible with XEmacs so let's case against loading there +(if (and (file-exists-p "/usr/share/emacs/site-lisp/agda/agda2.el") (not (string-match "XEmacs" emacs-version))) + (load-file "/usr/share/emacs/site-lisp/agda/agda2.el") +)