--- agda-stdlib-0.3.orig/debian/copyright +++ agda-stdlib-0.3/debian/copyright @@ -0,0 +1,39 @@ +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 + +Files: debian/watcher.sh +Copyright: Released into the public domain by original author, + Ian Lynagh , and therefore copyright is disclaimed +License: PD + +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,79 @@ +Source: agda-stdlib +Priority: extra +Section: libs +Maintainer: Iain Lane +Build-Depends: debhelper (>= 7.0.50~), + procps | hurd, + 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/agda-stdlib-doc.docs +++ agda-stdlib-0.3/debian/agda-stdlib-doc.docs @@ -0,0 +1 @@ +html/ --- 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/rules +++ agda-stdlib-0.3/debian/rules @@ -0,0 +1,23 @@ +#!/usr/bin/make -f + +override_dh_auto_clean: + find $(CURDIR) -name "*.agdai" -delete + rm -rf $(CURDIR)/html + dh_auto_clean + +override_dh_auto_build: + sh $(CURDIR)/debian/watcher.sh "$$PPID" "$(CURDIR)" "$(CURDIR)/build-stamp" 'agda' & + 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/watcher.sh +++ agda-stdlib-0.3/debian/watcher.sh @@ -0,0 +1,44 @@ +#!/bin/sh + +if [ "$#" -ne 4 ] +then + echo "Watcher: Bad args: $#" + exit 1 +fi + +CHECK_PID=$1 +DIR="$2" +FILE="$3" +GREP_FOR="$4" + +echo "Watcher: Check PID: $CHECK_PID" +echo "Watcher: Directory: $DIR" +echo "Watcher: File: $FILE" +echo "Watcher: Grep for: $GREP_FOR" + +if [ -d "$DIR" ]; then + if [ -f "$DIR/watcher-lock" ]; then + echo "Watcher: not spawning as lock in place" + exit 1 + else + echo "Watcher: creating lock" + touch $DIR/watcher-lock + fi +fi + +# If the PID we are told still exists (our caller is still running), +# the directory we are told (the working directory still exists) and +# the file we are told doesn't exist (the build stamp hasn't been created) +# keep going +while ps "$CHECK_PID" > /dev/null && + [ -d "$DIR" ] && + [ ! -f "$FILE" ] +do + sleep 600 + echo "Watcher: Tick." + ps ux | grep -- "$GREP_FOR" | grep -v grep +done + +echo "Watcher: Terminating." +echo "Watcher: Removing lock" +[ -f $DIR/watcher-lock ] && rm $DIR/watcher-lock --- 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/compat +++ agda-stdlib-0.3/debian/compat @@ -0,0 +1 @@ +7 --- agda-stdlib-0.3.orig/debian/changelog +++ agda-stdlib-0.3/debian/changelog @@ -0,0 +1,37 @@ +agda-stdlib (0.3-3fakesync) maverick; urgency=low + + * Fakesync from Debian unstable due to orig.tar.gz mismatch + + -- Iain Lane Tue, 25 May 2010 22:13:02 +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