--- agda-stdlib-0.5.orig/debian/copyright +++ agda-stdlib-0.5/debian/copyright @@ -0,0 +1,34 @@ +Format-Specification: http://svn.debian.org/wsvn/dep/web/deps/dep5.mdwn?rev=135&sc=0 +Name: Agda standard library +Maintainer: Nils Anders Danielsson +Upstream-Source: http://wiki.portal.chalmers.se/agda/agda.php?n=Libraries.StandardLibrary + +Files: * +Copyright: 2007-2011 Nils Anders Danielsson, Ulf Norell, Shin-Cheng Mu, Samuel + Bronson, Dan Doel, Patrik Jansson, Liang-Ting Chen, Jean-Philippe + Bernardy, Andrés Sicard-Ramírez, Nicolas Pouillard, Darin Morrison +License: MIT + +Files: debian/* +Copyright: 2010, Iain Lane +License: MIT + +License: MIT + 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. --- agda-stdlib-0.5.orig/debian/control +++ agda-stdlib-0.5/debian/control @@ -0,0 +1,80 @@ +Source: agda-stdlib +Priority: extra +Section: libs +Maintainer: Iain Lane +Build-Depends: debhelper (>= 7.0.50~), + agda-bin (>= 2.2.10), + agda-bin (<< 2.2.10.1~), + libghc-agda-dev (>= 2.2.10), + libghc-agda-dev (<< 2.2.10.1~) +Standards-Version: 3.9.2 +Vcs-Browser: http://git.debian.org/?p=collab-maint/agda-stdlib.git +Vcs-Git: git://git.debian.org/git/collab-maint/agda-stdlib.git +Homepage: http://wiki.portal.chalmers.se/agda/ + +Package: agda-stdlib +Architecture: all +Depends: ${misc:Depends}, + libghc-agda-dev (>= 2.2.10), + libghc-agda-dev (<< 2.2.10.1~) +Enhances: agda-mode +Description: standard library 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. + . + The Agda standard library contains modules for many common data structures and + proof patterns. Modules provided include: + - Algebra: Specifying and reasoning about abstract algebraic structures + - Category: Using idioms from category theory to structure functional programs + - Coinduction: Support for programming coindutively + - Data: Data types and properties about data types + - Foreign: Relating to the foreign function interface + - Induction: A general framework for induction + - IO: Input/output related functions + - Level: Universe levels + - Relations: Properties of and proofs about relations + - Size: Sizes used by the sized types mechanism + . + This package contains the complete library. + +Package: agda-stdlib-doc +Architecture: all +Section: doc +Depends: ${misc:Depends} +Suggests: agda-stdlib +Description: standard library for Agda — 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. + . + The Agda standard library contains modules for many common data structures and + proof patterns. Modules provided include: + - Algebra: Specifying and reasoning about abstract algebraic structures + - Category: Using idioms from category theory to structure functional programs + - Coinduction: Support for programming coindutively + - Data: Data types and properties about data types + - Foreign: Relating to the foreign function interface + - Induction: A general framework for induction + - IO: Input/output related functions + - Level: Universe levels + - Relations: Properties of and proofs about relations + - Size: Sizes used by the sized types mechanism + . + This package contains the hyperlinked library documentation. --- agda-stdlib-0.5.orig/debian/watch +++ agda-stdlib-0.5/debian/watch @@ -0,0 +1,3 @@ +version=3 + +http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary http://www.cse.chalmers.se/~nad/software/lib-(.*).tar.gz --- agda-stdlib-0.5.orig/debian/agda-stdlib-doc.docs +++ agda-stdlib-0.5/debian/agda-stdlib-doc.docs @@ -0,0 +1 @@ +html/ --- agda-stdlib-0.5.orig/debian/agda-stdlib.install +++ agda-stdlib-0.5/debian/agda-stdlib.install @@ -0,0 +1,3 @@ +src/* usr/share/agda-stdlib/ +debian/60agda-stdlib.el etc/emacs/site-start.d/ + --- agda-stdlib-0.5.orig/debian/rules +++ agda-stdlib-0.5/debian/rules @@ -0,0 +1,19 @@ +#!/usr/bin/make -f + +override_dh_auto_clean: + find $(CURDIR) -name "*.agdai" -delete + rm -rf $(CURDIR)/html + dh_auto_clean + +override_dh_auto_build: + agda +RTS -K1G -RTS -i $(CURDIR) -i $(CURDIR)/src $(CURDIR)/Everything.agda + agda --html -i $(CURDIR) -i $(CURDIR)/src $(CURDIR)/README.agda + +# Don't use upstream's 'make install' +override_dh_auto_install: + +override_dh_auto_test: + agda -i $(CURDIR) -i $(CURDIR)/src README.agda + +%: + dh $@ --- agda-stdlib-0.5.orig/debian/60agda-stdlib.el +++ agda-stdlib-0.5/debian/60agda-stdlib.el @@ -0,0 +1,5 @@ +;; This will be overwritten if the user customises the agda2-include-dirs +;; variable in his/her own session. But that is probably the intended behaviour +;; anyway. + +(setq agda2-include-dirs '("." "/usr/share/agda-stdlib")) --- agda-stdlib-0.5.orig/debian/compat +++ agda-stdlib-0.5/debian/compat @@ -0,0 +1 @@ +7 --- agda-stdlib-0.5.orig/debian/changelog +++ agda-stdlib-0.5/debian/changelog @@ -0,0 +1,54 @@ +agda-stdlib (0.5-1) unstable; urgency=low + + * [9251e0b] Imported Upstream version 0.5 + * [ba20206] Make package architecture independent (Closes: #573807, #598708, + #599958) + * [2c82171] Add watch file + * [0518fa6] No longer need procps | hurd BD as we no longer have the ticker + * [daf2445] Don't use upstream's make install — handled ourselves by + dh_install + * [1b86533] Update watchfile to point at new location + * [637f47d] Remove debian/gbp.conf as we are no longer building for exp + * [cc88671] Require Agda 2.2.10 + * [e99dab5] Set maximum stack size to 1G to prevent overflows in the build + * [251cd1d] Run the test suite manually + * [a7db697] Set the variable in the emacs loading script properly + * [540ca3f] Improve short description + * [6b3e794] Add dependencies on compatible versions of the Agda library + * [7127678] Standards-Version bump to 3.9.2, no changes required + * [9d0ae30] Update to use ghc instead of ghc6 + * [3f6879a] Set Maintainer to my d.o email address + + -- Iain Lane Tue, 24 May 2011 10:26:15 +0100 + +agda-stdlib (0.3-3) unstable; urgency=low + + [ Iain Lane ] + * debian/control: Add missing procps | hurd build-dep so that ps is available + to run the ticker. + + -- Marco Túlio Gontijo e Silva Tue, 02 Mar 2010 20:56:49 -0300 + +agda-stdlib (0.3-2) unstable; urgency=low + + [ Iain Lane ] + * debian/control: Fix short descriptions (too long, one said "profiling" + instead of "documentation") + * debian/rules, debian/control: No need to use upstream's buildsys. This only + builds Everything.agda which is already included in the distribution + anyway. Also trim GHC and filepath from build-deps as these aren't needed + now. This bypassing is required because upstream's buildsys invokes + runhaskell, which isn't available everywhere. (Closes: #569262) + * debian/rules: Disable upstream tests for the same reason as above. We + typecheck the same file, README.agda, to generate the documentation + anyway so this has no negative effect. + * debian/rules, debian/watcher.sh: Add a ticker to the build to avoid + timeouts on some slow architectures. + + -- Marco Túlio Gontijo e Silva Sat, 27 Feb 2010 09:05:52 -0300 + +agda-stdlib (0.3-1) unstable; urgency=low + + * Initial release. (Closes: #522914) + + -- Iain Lane Fri, 08 Jan 2010 23:35:09 +0000