Agda is a proof assistant. It is an interactive system for writing andchecking 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, Matita and NuPRL http://wiki.portal.chalmers.se/agda Jacula Fix: --- hs-Agda-executable.shar ends here -----OAXaVIusuIgMmMJR9jg4GkRObw9vW9bInA7L6dSFtUJ2y10a Content-Type: text/plain; name="hs-Agda.shar" Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename="hs-Agda.shar" # This is a shell archive. Save it in a file, remove anything before # this line, and then unpack it by entering "sh file". Note, it may # create directories; files and directories will be owned by you and # have default permissions. # # This archive contains: # # hs-Agda # hs-Agda/Makefile # hs-Agda/distinfo # hs-Agda/pkg-plist # hs-Agda/pkg-descr # echo c - hs-Agda mkdir -p hs-Agda > /dev/null 2>&1 echo x - hs-Agda/Makefile sed 's/^X//' >hs-Agda/Makefile << '0dee46eaa4d4865fbf85cb71edc52cfa' X# New ports collection makefile for: hs-Agda X# Date created: December 20 2009 X# Whom: Giuseppe Pilichi aka Jacula Modyun <jacula@gmail.com> X# X XPORTNAME= Agda XPORTVERSION= 2.2.6 XCATEGORIES= math haskell XMASTER_SITES= http://hackage.haskell.org/packages/archive/${PORTNAME}/${PORTVERSION}/ XPKGNAMEPREFIX= hs- X XMAINTAINER= jacula@gmail.com XCOMMENT= A functional programming language and proof assistant X XBUILD_DEPENDS+= ghc:${PORTSDIR}/lang/ghc \ X hs-QuickCheck>=2.1.0.2:${PORTSDIR}/devel/hs-QuickCheck \ X hs-binary-ghc>=0.4.4:${PORTSDIR}/devel/hs-binary-ghc \ X hs-zlib>=0.4.0.1:${PORTSDIR}/archivers/hs-zlib \ X hs-haskeline>=0.3:${PORTSDIR}/devel/hs-haskeline \ X hs-utf8-string-ghc>=0.1:${PORTSDIR}/devel/hs-utf8-string-ghc \ X hs-happy>=1.15:${PORTSDIR}/devel/hs-happy \ X hs-alex>=2.0.1:${PORTSDIR}/devel/hs-alex XRUN_DEPENDS+= ghc:${PORTSDIR}/lang/ghc \ X hs-QuickCheck>=2.1.0.2:${PORTSDIR}/devel/hs-QuickCheck \ X hs-binary-ghc>=0.4.4:${PORTSDIR}/devel/hs-binary-ghc \ X hs-zlib>=0.4.0.1:${PORTSDIR}/archivers/hs-zlib \ X hs-haskeline>=0.3:${PORTSDIR}/devel/hs-haskeline \ X hs-utf8-string-ghc>=0.1:${PORTSDIR}/devel/hs-utf8-string-ghc X XLIB_DEPENDS+= gmp.8:${PORTSDIR}/math/libgmp4 X XUSE_ICONV= yes X XGHC_VERSION= 6.10.4 XAGDA_VERSION= ${PORTVERSION} X XGHC_CMD= ${LOCALBASE}/bin/ghc XSETUP_CMD= ./setup X XDATADIR= ${PREFIX}/share/${DISTNAME} XDOCSDIR= ${PREFIX}/share/doc/${DISTNAME} XAGDA_LIBDIR_REL= lib/${DISTNAME} X XPLIST_SUB= GHC_VERSION=${GHC_VERSION} \ X AGDA_VERSION=${AGDA_VERSION} \ X AGDA_LIBDIR_REL=${AGDA_LIBDIR_REL} X X.if defined(NOPORTDOCS) XPLIST_SUB+= NOPORTDOCS="" X.else XPLIST_SUB+= NOPORTDOCS="@comment " X.endif X X.if !defined(NOPORTDOCS) X XPORT_HADDOCK!= (cd ${.CURDIR}/../../lang/ghc && ${MAKE} -V PORT_HADDOCK) X.if !empty(PORT_HADDOCK:M?0) XBUILD_DEPENDS+= haddock:${PORTSDIR}/devel/hs-haddock X.endif XBUILD_DEPENDS+= HsColour:${PORTSDIR}/print/hs-hscolour X XHSCOLOUR_VERSION= 1.15 XHSCOLOUR_DATADIR= ${PREFIX}/share/hscolour-${HSCOLOUR_VERSION} X XPORTDOCS= * X.endif X X.SILENT: X Xdo-configure: X cd ${WRKSRC} && ${GHC_CMD} --make Setup.hs -o setup -package Cabal \ X && ${SETUP_CMD} configure --haddock-options=-w --prefix=${PREFIX} X Xdo-build: X cd ${WRKSRC} && ${SETUP_CMD} build \ X && ${SETUP_CMD} register --gen-script X X.if !defined(NOPORTDOCS) X cd ${WRKSRC} && ${SETUP_CMD} haddock --hyperlink-source --executables \ X --hscolour-css=${HSCOLOUR_DATADIR}/hscolour.css X.endif X Xdo-install: X cd ${WRKSRC} && ${SETUP_CMD} install \ X && ${INSTALL_SCRIPT} register.sh ${PREFIX}/${AGDA_LIBDIR_REL}/register.sh \ X && ${INSTALL_DATA} README ${DATADIR} X cd ${WRKSRC}/doc && ${COPYTREE_SHARE} \* ${DATADIR} X Xpost-install: X ${RM} -f ${PREFIX}/lib/ghc-${GHC_VERSION}/package.conf.old X X.include <bsd.port.mk> 0dee46eaa4d4865fbf85cb71edc52cfa echo x - hs-Agda/distinfo sed 's/^X//' >hs-Agda/distinfo << '4efcf5355fbfb3c439ae0cd74aca03f6' XMD5 (Agda-2.2.6.tar.gz) = 9d598b507490ddd1815b3cb33c8c283e XSHA256 (Agda-2.2.6.tar.gz) = e9268a61db30fc0f22f7e1fbc78673cd3e0d1bf2dd40ee5cf809635ca40fca78 XSIZE (Agda-2.2.6.tar.gz) = 429015 4efcf5355fbfb3c439ae0cd74aca03f6 echo x - hs-Agda/pkg-plist sed 's/^X//' >hs-Agda/pkg-plist << '52c5ceada381774847cf9e93e1eacf35' Xbin/agda-mode X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Auto/Auto.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Auto/Convert.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Auto/NarrowingSearch.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Auto/Print.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Auto/SearchControl.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Auto/Syntax.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Auto/Typecheck.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Compiler/Agate/Classify.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Compiler/Agate/Common.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Compiler/Agate/Main.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Compiler/Agate/OptimizedPrinter.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Compiler/Agate/TranslateName.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Compiler/Agate/UntypedPrinter.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Compiler/Alonzo/Haskell.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Compiler/Alonzo/Main.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Compiler/Alonzo/Names.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Compiler/Alonzo/PatternMonad.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Compiler/HaskellTypes.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Compiler/MAlonzo/Compiler.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Compiler/MAlonzo/Encode.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Compiler/MAlonzo/Misc.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Compiler/MAlonzo/Pretty.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Compiler/MAlonzo/Primitives.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Interaction/BasicOps.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Interaction/CommandLine/CommandLine.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Interaction/Exceptions.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Interaction/FindFile.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Interaction/GhciTop.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Interaction/Highlighting/Emacs.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Interaction/Highlighting/Generate.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Interaction/Highlighting/HTML.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Interaction/Highlighting/Precise.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Interaction/Highlighting/Range.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Interaction/Highlighting/Vim.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Interaction/Imports.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Interaction/MakeCase.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Interaction/Monad.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Interaction/Options.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Main.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Abstract.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Abstract/Name.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Abstract/Pretty.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Abstract/Views.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Common.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Concrete.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Concrete/Definitions.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Concrete/Name.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Concrete/Operators.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Concrete/Operators/Parser.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Concrete/Pretty.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Fixity.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Info.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Internal.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Internal/Generic.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Internal/Pattern.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Literal.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Parser.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Parser/Alex.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Parser/Comments.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Parser/Layout.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Parser/LexActions.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Parser/Lexer.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Parser/LookAhead.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Parser/Monad.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Parser/Parser.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Parser/StringLiterals.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Parser/Tokens.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Position.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Scope/Base.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Scope/Monad.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Strict.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Translation/AbstractToConcrete.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Translation/ConcreteToAbstract.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Translation/InternalToAbstract.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Termination/CallGraph.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Termination/Lexicographic.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Termination/Matrix.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Termination/Semiring.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Termination/TermCheck.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Termination/Termination.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Tests.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecker.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Abstract.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Constraints.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Conversion.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Coverage.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Coverage/Match.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/DisplayForm.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Empty.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Errors.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/EtaContract.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Free.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Implicit.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Injectivity.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Level.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/MetaVars.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/MetaVars/Occurs.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Monad.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Monad/Base.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Monad/Builtin.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Monad/Closure.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Monad/Constraints.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Monad/Context.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Monad/Debug.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Monad/Env.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Monad/Exception.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Monad/Imports.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Monad/MetaVars.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Monad/Mutual.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Monad/Open.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Monad/Options.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Monad/Signature.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Monad/SizedTypes.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Monad/State.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Monad/Statistics.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Monad/Trace.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Patterns/Match.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Polarity.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Positivity.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Pretty.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Primitive.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Rebind.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Records.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Reduce.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Rules/Builtin.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Rules/Data.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Rules/Decl.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Rules/Def.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Rules/LHS.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Rules/LHS/Implicit.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Rules/LHS/Instantiate.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Rules/LHS/Problem.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Rules/LHS/Split.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Rules/LHS/Unify.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Rules/Record.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Rules/Term.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Serialise.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/SizedTypes.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Substitute.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Telescope.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Test/Generators.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Tests.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/With.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/Char.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/Either.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/FileName.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/Fresh.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/Function.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/Generics.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/Graph.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/Hash.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/IO/Binary.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/IO/Locale.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/IO/UTF8.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/Impossible.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/List.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/Map.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/Maybe.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/Monad.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/Permutation.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/Pointer.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/Pretty.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/QuickCheck.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/ReadP.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/SemiRing.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/Size.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/String.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/Suffix.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/TestHelpers.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/Trace.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/Trie.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/Tuple.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/Unicode.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/Warshall.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Version.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/HSAgda-%%AGDA_VERSION%%.o X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Paths_Agda.hi X%%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/libHSAgda-%%AGDA_VERSION%%.a X%%AGDA_LIBDIR_REL%%/register.sh X%%DATADIR%%/Agda.css X%%DATADIR%%/README X%%DATADIR%%/emacs-mode/agda-input.el X%%DATADIR%%/emacs-mode/agda2-abbrevs.el X%%DATADIR%%/emacs-mode/agda2-highlight.el X%%DATADIR%%/emacs-mode/agda2-mode.el X%%DATADIR%%/emacs-mode/agda2.el X%%DATADIR%%/emacs-mode/annotation.el X%%DATADIR%%/emacs-mode/eri.el X%%DATADIR%%/release-notes/2-2-0.txt X%%DATADIR%%/release-notes/2-2-2.txt X%%DATADIR%%/release-notes/2-2-4.txt X%%DATADIR%%/release-notes/2-2-6.txt X%%NOPORTDOCS%%%%DOCSDIR%%/LICENSE X%%NOPORTDOCS%%@dirrmtry %%DOCSDIR%% X@dirrm %%DATADIR%%/release-notes X@dirrm %%DATADIR%%/emacs-mode X@dirrmtry %%DATADIR%% X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils/IO X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Utils X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Test X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Rules/LHS X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Rules X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Patterns X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Monad X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/MetaVars X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking/Coverage X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/TypeChecking X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Termination X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Translation X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Scope X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Parser X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Internal X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Concrete/Operators X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Concrete X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax/Abstract X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Syntax X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Interaction/Highlighting X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Interaction/CommandLine X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Interaction X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Compiler/MAlonzo X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Compiler/Alonzo X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Compiler/Agate X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Compiler X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda/Auto X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%%/Agda X@dirrm %%AGDA_LIBDIR_REL%%/ghc-%%GHC_VERSION%% X@dirrm %%AGDA_LIBDIR_REL%% X@exec /bin/sh %D/%%AGDA_LIBDIR_REL%%/register.sh X@exec /bin/rm -f %D/lib/ghc-%%GHC_VERSION%%/package.conf.old X@unexec %D/bin/ghc-pkg unregister Agda X@unexec /bin/rm -f %D/lib/ghc-%%GHC_VERSION%%/package.conf.old 52c5ceada381774847cf9e93e1eacf35 echo x - hs-Agda/pkg-descr sed 's/^X//' >hs-Agda/pkg-descr << 'df32a9fa912dff38324498ab705f4ff4' XAgda is a dependently typed functional programming language: It has inductive Xfamilies, which are similar to Haskell's GADTs, but they can be indexed by Xvalues and not just types. It also has parameterised modules, mixfix operators, XUnicode characters, and an interactive Emacs interface (the type checker can Xassist in the development of your code). X XAgda is also a proof assistant: It is an interactive system for writing and Xchecking proofs. Agda is based on intuitionistic type theory, a foundational Xsystem for constructive mathematics developed by the Swedish logician Per XMartin-Lof. It has many similarities with other proof assistants based on Xdependent types, such as Coq, Epigram and NuPRL. X XNote that if you want to use the command-line program (agda), then Xyou should also install the Agda-executable package. The Agda Xpackage includes an Emacs mode for Agda, but you need to set up the XEmacs mode yourself (for instance by running agda-mode setup; see Xthe README). X XNote also that this library does not follow the package versioning Xpolicy, because the library is only intended to be used by the Emacs Xmode and the Agda-executable package. X XWWW: http://wiki.portal.chalmers.se/agda/ df32a9fa912dff38324498ab705f4ff4 exit
Responsible Changed From-To: freebsd-ports-bugs->haskell haskell@ wants this port PRs (via the GNATS Auto Assign Tool)
pgj 2010-01-04 03:24:25 UTC FreeBSD ports repository Modified files: math Makefile Added files: math/hs-Agda Makefile distinfo pkg-descr pkg-message pkg-plist Log: Agda is a dependently typed functional programming language: It has inductive families, which are similar to 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-Lof. It has many similarities with other proof assistants based on dependent types, such as Coq, Epigram and NuPRL. WWW: http://wiki.portal.chalmers.se/agda/ PR: ports/142141 Submitted by: Jacula Modyun <jacula(at)gmail.com> Revision Changes Path 1.625 +1 -0 ports/math/Makefile 1.1 +109 -0 ports/math/hs-Agda/Makefile (new) 1.1 +3 -0 ports/math/hs-Agda/distinfo (new) 1.1 +13 -0 ports/math/hs-Agda/pkg-descr (new) 1.1 +9 -0 ports/math/hs-Agda/pkg-message (new) 1.1 +217 -0 ports/math/hs-Agda/pkg-plist (new) _______________________________________________ cvs-all@freebsd.org mailing list http://lists.freebsd.org/mailman/listinfo/cvs-all To unsubscribe, send any mail to "cvs-all-unsubscribe@freebsd.org"
pgj 2010-01-04 03:26:20 UTC FreeBSD ports repository Modified files: math Makefile Added files: math/hs-Agda-executable Makefile distinfo pkg-descr pkg-plist Log: This package provides a command-line program for type-checking and compiling Agda programs. The program can also generate hyperlinked, highlighted HTML files from Agda sources. WWW: http://wiki.portal.chalmers.se/agda/ PR: ports/142141 Submitted by: Jacula Modyun <jacula(at)gmail.com> Revision Changes Path 1.626 +1 -0 ports/math/Makefile 1.1 +75 -0 ports/math/hs-Agda-executable/Makefile (new) 1.1 +3 -0 ports/math/hs-Agda-executable/distinfo (new) 1.1 +5 -0 ports/math/hs-Agda-executable/pkg-descr (new) 1.1 +4 -0 ports/math/hs-Agda-executable/pkg-plist (new) _______________________________________________ cvs-all@freebsd.org mailing list http://lists.freebsd.org/mailman/listinfo/cvs-all To unsubscribe, send any mail to "cvs-all-unsubscribe@freebsd.org"
State Changed From-To: open->closed The ports have been committed with minor nits. Thank you for your submissions!