--- agda-stdlib-0.3.orig/debian/agda-stdlib-doc.docs +++ agda-stdlib-0.3/debian/agda-stdlib-doc.docs @@ -0,0 +1 @@ +html/ --- agda-stdlib-0.3.orig/debian/copyright +++ agda-stdlib-0.3/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-2009 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.3.orig/debian/control +++ agda-stdlib-0.3/debian/control @@ -0,0 +1,78 @@ +Source: agda-stdlib +Priority: extra +Section: libs +Maintainer: Iain Lane +Build-Depends: debhelper (>= 7.0.50~), + agda-bin (>= 2.2.6), + agda-bin (<< 2.2.6.1~), + libghc6-agda-dev (>= 2.2.6), + libghc6-agda-dev (<< 2.2.6.1~) +Standards-Version: 3.8.4 +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: any +Depends: ${misc:Depends} +Enhances: agda-mode +Description: a dependently typed programming language - standard library + 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: a dependently typed 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. + . + 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.3.orig/debian/60agda-stdlib.el +++ agda-stdlib-0.3/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. +(custom-set-variables + '(agda2-include-dirs (quote ("." "/usr/lib/agda-stdlib/")))) --- agda-stdlib-0.3.orig/debian/rules +++ agda-stdlib-0.3/debian/rules @@ -0,0 +1,22 @@ +#!/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 -i $(CURDIR) -i $(CURDIR)/src $(CURDIR)/Everything.agda + # Can I easily make this happen only for the indep build? + # It's really not much overhead either way, but would be a nice improvement + agda --html -i $(CURDIR) -i $(CURDIR)/src $(CURDIR)/README.agda + +# disable "tests". This only typechecks README.agda, which we do to build the +# docs anyway. +# +# Upstream's test rule invokes runhaskell, which isn't available on all +# architectures and so causes an FTBFS. +override_dh_auto_test: + +%: + dh $@ --- agda-stdlib-0.3.orig/debian/agda-stdlib.install +++ agda-stdlib-0.3/debian/agda-stdlib.install @@ -0,0 +1,3 @@ +src/* usr/lib/agda-stdlib/ +debian/60agda-stdlib.el etc/emacs/site-start.d/ + --- agda-stdlib-0.3.orig/debian/changelog +++ agda-stdlib-0.3/debian/changelog @@ -0,0 +1,22 @@ +agda-stdlib (0.3-1ubuntu1) lucid; urgency=low + + * Upload to Lucid. Cannot immediately upload to sid as agda is tied up in a + GHC transition taking place. + * 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 becuase upstream's buildsys invokes + runhaskell, which isn't available everywhere. + * 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. + + -- Iain Lane Wed, 10 Feb 2010 10:45:04 +0000 + +agda-stdlib (0.3-1) unstable; urgency=low + + * Initial release. (Closes: #522914) + + -- Iain Lane Fri, 08 Jan 2010 23:35:09 +0000 --- agda-stdlib-0.3.orig/debian/compat +++ agda-stdlib-0.3/debian/compat @@ -0,0 +1 @@ +7