Cabal revisions of MiniAgda-0.2022.3.11
Hackage metadata revisions edit the .cabal file after upload; each diff below is one revision.
revision 1
-cabal-version: 2.4-name: MiniAgda-version: 0.2022.3.11-build-type: Simple-license: MIT-license-file: LICENSE-author: Andreas Abel and Karl Mehltretter-maintainer: Andreas Abel <andreas.abel@cse.gu.se>-homepage: http://www.cse.chalmers.se/~abela/miniagda/-bug-reports: https://github.com/andreasabel/miniagda/issues-category: Dependent types-synopsis: A toy dependently typed programming language with type-based termination.-description:- MiniAgda is a tiny dependently-typed programming language in the style- of Agda. It serves as a laboratory to test potential additions to the- language and type system of Agda. MiniAgda's termination checker is a- fusion of sized types and size-change termination and supports- coinduction. Equality incorporates eta-expansion at record and- singleton types. Function arguments can be declared as static; such- arguments are discarded during equality checking and compilation.-- Recent features include bounded size quantification and destructor- patterns for a more general handling of coinduction.--tested-with:- GHC == 9.2.2- GHC == 9.0.2- GHC == 8.10.7- GHC == 8.8.4- GHC == 8.6.5- GHC == 8.4.4- GHC == 8.2.2- GHC == 8.0.2- GHC == 7.10.3- GHC == 7.8.4- GHC == 7.6.3--extra-source-files:- CHANGELOG- README.md- Makefile- src/Makefile--data-files:- test/fail/Makefile- test/succeed/Makefile- test/**/*.ma- test/*.goldplate- test/**/*.golden- test/**/*.err- lib/*.ma--source-repository head- type: git- location: https://github.com/andreasabel/miniagda--executable miniagda- hs-source-dirs: src- build-depends: array >= 0.3 && < 0.6- , base >= 4.6 && < 5- , containers >= 0.3 && < 0.7- , haskell-src-exts >= 1.21 && < 1.22- -- haskell-src-exts is a nervous package with incompatibilities- -- in every new version, thus, we need tight bounds.- , mtl >= 2.2.2 && < 2.4- , pretty >= 1.0 && < 1.2- , transformers- build-tool-depends: happy:happy >= 1.15 && < 2- , alex:alex >= 3.0 && < 4- default-language: Haskell98- default-extensions: CPP- MultiParamTypeClasses- TypeSynonymInstances- FlexibleInstances- FlexibleContexts- GeneralizedNewtypeDeriving- NoMonomorphismRestriction- PatternGuards- TupleSections- NamedFieldPuns- LambdaCase- main-is: Main.hs- other-modules: Abstract- Collection- Concrete- Eval- Extract- HsSyntax- Lexer- Parser- Polarity- PrettyTCM- ScopeChecker- Semiring- SparseMatrix- TCM- Termination- ToHaskell- Tokens- TraceError- TreeShapedOrder- TypeChecker- Util- Value- Warshall-- -- TODO: Warning-free- -- ghc-options: -Wall- -- -fno-warn-type-defaults- -- -fno-warn-dodgy-imports- -- -fno-warn-unused-binds- -- -fno-warn-unused-matches- -- -fno-warn-name-shadowing- -- -fno-warn-incomplete-patterns-- if impl(ghc >= 8.0)- ghc-options: -Wcompat- if impl(ghc >= 9.2)- ghc-options: -Wno-incomplete-uni-patterns--test-suite test- type: exitcode-stdio-1.0- hs-source-dirs: test- main-is: GoldplateTests.hs- default-language: Haskell2010- ghc-options: -threaded- build-depends: base >= 4.11- -- goldplate requires ghc >= 8.4- , process- build-tool-depends: goldplate:goldplate >= 0.2- -- goldplate-0.2.0 adds "working_directory"- , MiniAgda:miniagda- -- We also need to depend on ourselves since goldplate calls us.+cabal-version: 2.4 +name: MiniAgda +version: 0.2022.3.11 +x-revision: 1 +build-type: Simple +license: MIT +license-file: LICENSE +author: Andreas Abel and Karl Mehltretter +maintainer: Andreas Abel <andreas.abel@cse.gu.se> +homepage: http://www.cse.chalmers.se/~abela/miniagda/ +bug-reports: https://github.com/andreasabel/miniagda/issues +category: Dependent types +synopsis: A toy dependently typed programming language with type-based termination. +description: + MiniAgda is a tiny dependently-typed programming language in the style + of Agda. It serves as a laboratory to test potential additions to the + language and type system of Agda. MiniAgda's termination checker is a + fusion of sized types and size-change termination and supports + coinduction. Equality incorporates eta-expansion at record and + singleton types. Function arguments can be declared as static; such + arguments are discarded during equality checking and compilation. + + Recent features include bounded size quantification and destructor + patterns for a more general handling of coinduction. + +tested-with: + GHC == 9.2.2 + GHC == 9.0.2 + GHC == 8.10.7 + GHC == 8.8.4 + GHC == 8.6.5 + GHC == 8.4.4 + GHC == 8.2.2 + GHC == 8.0.2 + GHC == 7.10.3 + GHC == 7.8.4 + GHC == 7.6.3 + +extra-source-files: + CHANGELOG + README.md + Makefile + src/Makefile + +data-files: + test/fail/Makefile + test/succeed/Makefile + test/**/*.ma + test/*.goldplate + test/**/*.golden + test/**/*.err + lib/*.ma + +source-repository head + type: git + location: https://github.com/andreasabel/miniagda + +executable miniagda + hs-source-dirs: src + build-depends: array >= 0.3 && < 0.6 + , base >= 4.6 && < 5 + , containers >= 0.3 && < 1 + , haskell-src-exts >= 1.21 && < 1.22 + -- haskell-src-exts is a nervous package with incompatibilities + -- in every new version, thus, we need tight bounds. + , mtl >= 2.2.2 && < 2.4 + , pretty >= 1.0 && < 1.2 + , transformers + build-tool-depends: happy:happy >= 1.15 && < 3 + , alex:alex >= 3.0 && < 4 + default-language: Haskell98 + default-extensions: CPP + MultiParamTypeClasses + TypeSynonymInstances + FlexibleInstances + FlexibleContexts + GeneralizedNewtypeDeriving + NoMonomorphismRestriction + PatternGuards + TupleSections + NamedFieldPuns + LambdaCase + main-is: Main.hs + other-modules: Abstract + Collection + Concrete + Eval + Extract + HsSyntax + Lexer + Parser + Polarity + PrettyTCM + ScopeChecker + Semiring + SparseMatrix + TCM + Termination + ToHaskell + Tokens + TraceError + TreeShapedOrder + TypeChecker + Util + Value + Warshall + + -- TODO: Warning-free + -- ghc-options: -Wall + -- -fno-warn-type-defaults + -- -fno-warn-dodgy-imports + -- -fno-warn-unused-binds + -- -fno-warn-unused-matches + -- -fno-warn-name-shadowing + -- -fno-warn-incomplete-patterns + + if impl(ghc >= 8.0) + ghc-options: -Wcompat + if impl(ghc >= 9.2) + ghc-options: -Wno-incomplete-uni-patterns + +test-suite test + type: exitcode-stdio-1.0 + hs-source-dirs: test + main-is: GoldplateTests.hs + default-language: Haskell2010 + ghc-options: -threaded + build-depends: base >= 4.11 + -- goldplate requires ghc >= 8.4 + , process + build-tool-depends: goldplate:goldplate >= 0.2 + -- goldplate-0.2.0 adds "working_directory" + , MiniAgda:miniagda + -- We also need to depend on ourselves since goldplate calls us.