mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-08-16 12:10:39 +03:00
479 lines
15 KiB
Plaintext
479 lines
15 KiB
Plaintext
Cabal-Version: 2.4
|
|
Name: idris
|
|
Version: 1.3.2
|
|
License: BSD-3-Clause
|
|
License-file: LICENSE
|
|
Author: Edwin Brady
|
|
Maintainer: Edwin Brady <eb@cs.st-andrews.ac.uk>
|
|
Homepage: https://www.idris-lang.org/
|
|
Bug-reports: https://github.com/idris-lang/Idris-dev/issues
|
|
|
|
Stability: Beta
|
|
Category: Compilers/Interpreters, Dependent Types
|
|
Synopsis: Functional Programming Language with Dependent Types
|
|
Description: Idris is a general purpose language with full dependent types.
|
|
It is compiled, with eager evaluation.
|
|
Dependent types allow types to be predicated on values,
|
|
meaning that some aspects of a program's behaviour can be
|
|
specified precisely in the type. The language is closely
|
|
related to Epigram and Agda. There is a tutorial at
|
|
<https://www.idris-lang.org/documentation>.
|
|
Features include:
|
|
.
|
|
* Full, first class, dependent types with dependent pattern matching
|
|
.
|
|
* where clauses, with rule, case expressions,
|
|
pattern matching let and lambda bindings
|
|
.
|
|
* Interfaces (similar to type classes), monad comprehensions
|
|
.
|
|
* do notation, idiom brackets, syntactic conveniences for lists,
|
|
tuples, dependent pairs
|
|
.
|
|
* Totality checking
|
|
.
|
|
* Coinductive types
|
|
.
|
|
* Indentation significant syntax, extensible syntax
|
|
.
|
|
* Cumulative universes
|
|
.
|
|
* Simple foreign function interface (to C)
|
|
.
|
|
* Hugs style interactive environment
|
|
|
|
Build-type: Custom
|
|
|
|
Tested-With: GHC == 7.10.3, GHC == 8.0.1
|
|
|
|
-- NOTE: due to https://github.com/haskell/cabal/issues/6125 the use of ** is
|
|
-- heavily discouraged.
|
|
Data-files: idrisdoc/styles.css
|
|
jsrts/jsbn/*.js
|
|
jsrts/*.js
|
|
jsrts/jsbn/LICENSE
|
|
rts/Makefile
|
|
rts/*.c
|
|
rts/seL4/*.c
|
|
rts/arduino/*.c
|
|
rts/windows/*.c
|
|
rts/windows/*.h
|
|
rts/*.h
|
|
rts/seL4/CMakeLists.txt
|
|
rts/seL4/README.md
|
|
|
|
Extra-doc-files:
|
|
CHANGELOG.md
|
|
CITATION.md
|
|
CONTRIBUTING.md
|
|
CONTRIBUTORS
|
|
README.md
|
|
RELEASE-CHECKS.md
|
|
idris-tutorial.pdf
|
|
man/idris.1
|
|
samples/effects/*.idr
|
|
samples/misc/*.idr
|
|
samples/tutorial/*.idr
|
|
samples/ST/*.idr
|
|
samples/ST/Graphics/*.idr
|
|
samples/ST/Net/*.idr
|
|
samples/misc/*.lidr
|
|
|
|
-- extra-source-files is generated by Setup.hs using `git --ls-files`.
|
|
Extra-source-files:
|
|
Makefile
|
|
config.mk
|
|
custom.mk-alldeps
|
|
mkpkg.sh
|
|
stack-shell.nix
|
|
stack.yaml
|
|
stylize.sh
|
|
win-release.sh
|
|
|
|
benchmarks/*.pl
|
|
benchmarks/fasta/*.idr
|
|
benchmarks/fasta/*.ipkg
|
|
benchmarks/pidigits/*.idr
|
|
benchmarks/pidigits/*.ipkg
|
|
benchmarks/quasigroups/*.idr
|
|
benchmarks/quasigroups/*.ipkg
|
|
benchmarks/trivial/*.idr
|
|
benchmarks/trivial/*.ipkg
|
|
benchmarks/quasigroups/board
|
|
|
|
icons/*.png
|
|
icons/*.ico
|
|
icons/*.rc
|
|
icons/*.svg
|
|
icons/*.xml
|
|
|
|
libs/**/*.idr
|
|
libs/**/*.ipkg
|
|
libs/**/*.txt
|
|
libs/Makefile
|
|
libs/base/Makefile
|
|
libs/contrib/Makefile
|
|
libs/effects/Makefile
|
|
libs/prelude/Makefile
|
|
libs/pruviloj/Makefile
|
|
|
|
scripts/generate-multi-ghc-travis-template
|
|
scripts/runidris
|
|
scripts/runidris-node
|
|
|
|
src/.ghci
|
|
|
|
test/*.md
|
|
test/*.hs
|
|
test/**/*.idr
|
|
test/**/*.lidr
|
|
test/**/*.ipkg
|
|
test/**/*.out
|
|
test/**/*.sh
|
|
test/**/*.c
|
|
test/**/*.h
|
|
test/**/*.in
|
|
test/**/*.txt
|
|
test/**/*.js
|
|
test/base001/Makefile
|
|
test/ffi004/theOtherType
|
|
test/ffi004/theType
|
|
test/scripts/timeout
|
|
|
|
source-repository head
|
|
type: git
|
|
location: git://github.com/idris-lang/Idris-dev.git
|
|
|
|
custom-setup
|
|
setup-depends:
|
|
Cabal >= 2.4 && < 3.1,
|
|
base >= 4 && <5,
|
|
directory,
|
|
filepath,
|
|
process
|
|
|
|
Flag FFI
|
|
Description: Build support for libffi
|
|
Default: False
|
|
manual: True
|
|
|
|
Flag GMP
|
|
Description: Use GMP for Integers
|
|
Default: False
|
|
manual: True
|
|
|
|
-- This flag determines whether to show Git hashes in version strings
|
|
-- Defaults to True because Hackage is a source release
|
|
Flag release
|
|
Description: This is an official release
|
|
Default: False
|
|
manual: True
|
|
|
|
Flag freestanding
|
|
Description: Build an Idris that doesn't use cabal
|
|
Default: False
|
|
manual: True
|
|
|
|
Flag CI
|
|
Description: Built everything using "-Werror", meant for CI-builds only
|
|
Default: False
|
|
manual: True
|
|
|
|
Flag execonly
|
|
Description: Build executables only, skip the libraries and RTS
|
|
Default: False
|
|
manual: True
|
|
|
|
Library
|
|
hs-source-dirs: src
|
|
Exposed-modules:
|
|
Idris.Core.Binary
|
|
, Idris.Core.CaseTree
|
|
, Idris.Core.Constraints
|
|
, Idris.Core.DeepSeq
|
|
, Idris.Core.Elaborate
|
|
, Idris.Core.Evaluate
|
|
, Idris.Core.Execute
|
|
, Idris.Core.ProofState
|
|
, Idris.Core.ProofTerm
|
|
, Idris.Core.TT
|
|
, Idris.Core.Typecheck
|
|
, Idris.Core.Unify
|
|
, Idris.Core.WHNF
|
|
|
|
, Idris.Elab.Utils
|
|
, Idris.Elab.Type
|
|
, Idris.Elab.AsPat
|
|
, Idris.Elab.Clause
|
|
, Idris.Elab.Data
|
|
, Idris.Elab.Record
|
|
, Idris.Elab.Interface
|
|
, Idris.Elab.Implementation
|
|
, Idris.Elab.Provider
|
|
, Idris.Elab.RunElab
|
|
, Idris.Elab.Transform
|
|
, Idris.Elab.Value
|
|
, Idris.Elab.Term
|
|
, Idris.Elab.Quasiquote
|
|
, Idris.Elab.Rewrite
|
|
|
|
, Idris.REPL.Browse
|
|
|
|
, Idris.AbsSyntax
|
|
, Idris.AbsSyntaxTree
|
|
, Idris.Apropos
|
|
, Idris.ASTUtils
|
|
, Idris.CaseSplit
|
|
, Idris.Chaser
|
|
, Idris.Colours
|
|
, Idris.Completion
|
|
, Idris.Coverage
|
|
, Idris.DSL
|
|
, Idris.DataOpts
|
|
, Idris.DeepSeq
|
|
, Idris.Delaborate
|
|
, Idris.Directives
|
|
, Idris.Docs
|
|
, Idris.Docstrings
|
|
, Idris.ElabDecls
|
|
, Idris.Erasure
|
|
, Idris.Error
|
|
, Idris.ErrReverse
|
|
, Idris.Help
|
|
, Idris.IBC
|
|
, Idris.IdeMode
|
|
, Idris.IdrisDoc
|
|
, Idris.Imports
|
|
, Idris.Info
|
|
, Idris.Info.Show
|
|
, Idris.Inliner
|
|
, Idris.Interactive
|
|
, Idris.Output
|
|
, Idris.Main
|
|
, Idris.ModeCommon
|
|
, Idris.Options
|
|
, Idris.Parser
|
|
, Idris.Parser.Data
|
|
, Idris.Parser.Expr
|
|
, Idris.Parser.Helpers
|
|
, Idris.Parser.Ops
|
|
, Idris.Parser.Stack
|
|
, Idris.PartialEval
|
|
, Idris.Primitives
|
|
, Idris.ProofSearch
|
|
, Idris.Prover
|
|
, Idris.Providers
|
|
, Idris.Reflection
|
|
, Idris.REPL
|
|
, Idris.REPL.Parser
|
|
, Idris.REPL.Commands
|
|
, Idris.Termination
|
|
, Idris.Transforms
|
|
, Idris.TypeSearch
|
|
, Idris.Unlit
|
|
, Idris.WhoCalls
|
|
, Idris.CmdOptions
|
|
|
|
, IRTS.Bytecode
|
|
, IRTS.CodegenC
|
|
, IRTS.CodegenCommon
|
|
, IRTS.CodegenJavaScript
|
|
, IRTS.Exports
|
|
, IRTS.JavaScript.AST
|
|
, IRTS.JavaScript.Name
|
|
, IRTS.JavaScript.Codegen
|
|
, IRTS.JavaScript.LangTransforms
|
|
, IRTS.JavaScript.Specialize
|
|
, IRTS.JavaScript.PrimOp
|
|
, IRTS.Compiler
|
|
, IRTS.Defunctionalise
|
|
, IRTS.DumpBC
|
|
, IRTS.Inliner
|
|
, IRTS.Lang
|
|
, IRTS.LangOpts
|
|
, IRTS.Portable
|
|
, IRTS.Simplified
|
|
, IRTS.System
|
|
|
|
, Idris.Package
|
|
, Idris.Package.Common
|
|
, Idris.Package.Parser
|
|
|
|
, Util.DynamicLinker
|
|
, Util.ScreenSize
|
|
, Util.System
|
|
|
|
Other-modules:
|
|
Util.Pretty
|
|
, Util.Net
|
|
|
|
, Paths_idris
|
|
, Version_idris
|
|
, Tools_idris
|
|
, BuildFlags_idris
|
|
|
|
-- Auto Generated
|
|
Autogen-modules: Paths_idris
|
|
, Version_idris
|
|
, Tools_idris
|
|
, BuildFlags_idris
|
|
|
|
Build-depends: base >=4 && <5
|
|
, aeson >= 0.6 && < 1.5
|
|
, annotated-wl-pprint >= 0.7 && < 0.8
|
|
, ansi-terminal < 0.11
|
|
, ansi-wl-pprint < 0.7
|
|
, array >= 0.4.0.1 && < 0.6
|
|
, base64-bytestring < 1.1
|
|
, binary >= 0.8.4.1 && < 0.9
|
|
, blaze-html >= 0.6.1.3 && < 0.10
|
|
, blaze-markup >= 0.5.2.1 && < 0.10
|
|
, bytestring < 0.11
|
|
, cheapskate >= 0.1.1.2 && < 0.2
|
|
, code-page >= 0.1 && < 0.3
|
|
, containers >= 0.5 && < 0.7
|
|
, deepseq < 1.5
|
|
, directory >= 1.2.2.0 && < 1.2.3.0 || > 1.2.3.0
|
|
, filepath < 1.5
|
|
, fingertree >= 0.1.4.1 && < 0.2
|
|
, haskeline >= 0.7 && < 0.8
|
|
, ieee754 >= 0.7 && < 0.9
|
|
, megaparsec >= 7.0.4 && < 9
|
|
, mtl >= 2.1 && < 2.3
|
|
, network >= 2.7 && < 3.1.2
|
|
, optparse-applicative >= 0.13 && < 0.16
|
|
, parser-combinators >= 1.0.0
|
|
, pretty < 1.2
|
|
, process < 1.7
|
|
, regex-tdfa >= 1.2
|
|
, safe >= 0.3.9
|
|
, split < 0.3
|
|
, terminal-size < 0.4
|
|
, text >=1.2.1.0 && < 1.4
|
|
, time >= 1.4 && < 2.0
|
|
, transformers >= 0.5 && < 0.6
|
|
, uniplate >=1.6 && < 1.7
|
|
, unordered-containers < 0.3
|
|
, utf8-string < 1.1
|
|
, vector < 0.13
|
|
, vector-binary-instances < 0.3
|
|
, zip-archive > 0.2.3.5 && < 0.5
|
|
, fsnotify >= 0.2 && < 0.4
|
|
, async < 2.3
|
|
|
|
if !impl(ghc >= 8.0)
|
|
Build-Depends: semigroups == 0.18.*
|
|
, fail == 4.9.0.*
|
|
|
|
Default-Language: Haskell2010
|
|
ghc-prof-options: -auto-all -caf-all
|
|
|
|
if os(windows)
|
|
build-depends: mintty >= 0.1 && < 0.2
|
|
, Win32 < 2.7
|
|
else
|
|
build-depends: unix < 2.8
|
|
if flag(FFI)
|
|
build-depends: libffi < 0.2
|
|
cpp-options: -DIDRIS_FFI
|
|
if flag(GMP)
|
|
build-depends: libffi < 0.2
|
|
extra-libraries: gmp
|
|
cpp-options: -DIDRIS_GMP
|
|
if flag(freestanding)
|
|
other-modules: Target_idris
|
|
autogen-modules: Target_idris
|
|
cpp-options: -DFREESTANDING
|
|
if flag(CI)
|
|
ghc-options: -Werror
|
|
|
|
Executable idris
|
|
Main-is: Main.hs
|
|
hs-source-dirs: main
|
|
|
|
Build-depends: idris
|
|
, base
|
|
, filepath
|
|
, directory
|
|
, haskeline >= 0.7
|
|
, transformers
|
|
|
|
Default-Language: Haskell2010
|
|
ghc-prof-options: -auto-all -caf-all
|
|
ghc-options: -threaded -rtsopts -funbox-strict-fields -with-rtsopts=-I0
|
|
|
|
Test-suite regression-and-feature-tests
|
|
Type: exitcode-stdio-1.0
|
|
Main-is: TestRun.hs
|
|
Other-modules: TestData
|
|
hs-source-dirs: test
|
|
|
|
Build-depends: idris
|
|
, base
|
|
, containers
|
|
, process
|
|
, time
|
|
, filepath
|
|
, directory
|
|
, haskeline >= 0.7
|
|
, optparse-applicative >= 0.13 && < 0.16
|
|
, tagged
|
|
, tasty >= 0.8
|
|
, tasty-golden >= 2.0
|
|
, tasty-rerun >= 1.0.0
|
|
, bytestring
|
|
, transformers
|
|
|
|
|
|
Default-Language: Haskell2010
|
|
ghc-prof-options: -auto-all -caf-all
|
|
ghc-options: -threaded -rtsopts -with-rtsopts=-N -funbox-strict-fields
|
|
|
|
Executable idris-codegen-c
|
|
Main-is: Main.hs
|
|
autogen-modules: Paths_idris
|
|
other-modules: Paths_idris
|
|
hs-source-dirs: codegen/idris-codegen-c
|
|
|
|
Build-depends: idris
|
|
, base
|
|
, filepath
|
|
, haskeline >= 0.7
|
|
, transformers
|
|
|
|
Default-Language: Haskell2010
|
|
ghc-prof-options: -auto-all -caf-all
|
|
ghc-options: -threaded -rtsopts -funbox-strict-fields
|
|
|
|
Executable idris-codegen-javascript
|
|
Main-is: Main.hs
|
|
autogen-modules: Paths_idris
|
|
other-modules: Paths_idris
|
|
hs-source-dirs: codegen/idris-codegen-javascript
|
|
|
|
Build-depends: idris
|
|
, base
|
|
, filepath
|
|
, haskeline >= 0.7
|
|
, transformers
|
|
|
|
Default-Language: Haskell2010
|
|
ghc-prof-options: -auto-all -caf-all
|
|
ghc-options: -threaded -rtsopts -funbox-strict-fields
|
|
|
|
Executable idris-codegen-node
|
|
Main-is: Main.hs
|
|
autogen-modules: Paths_idris
|
|
other-modules: Paths_idris
|
|
hs-source-dirs: codegen/idris-codegen-node
|
|
|
|
Build-depends: idris
|
|
, base
|
|
, filepath
|
|
, haskeline >= 0.7
|
|
, transformers
|
|
|
|
Default-Language: Haskell2010
|
|
ghc-prof-options: -auto-all -caf-all
|
|
ghc-options: -threaded -rtsopts -funbox-strict-fields
|