Cabal revisions of liquid-fixpoint-0.4.0.0
Hackage metadata revisions edit the .cabal file after upload; each diff below is one revision.
revision 1
-name: liquid-fixpoint-version: 0.4.0.0-Copyright: 2010-15 Ranjit Jhala, University of California, San Diego.-synopsis: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver-homepage: https://github.com/ucsd-progsys/liquid-fixpoint-license: BSD3-license-file: LICENSE-author: Ranjit Jhala, Niki Vazou, Eric Seidel-maintainer: jhala@cs.ucsd.edu-category: Language-build-type: Custom-cabal-version: >=1.10--description: This package is a Haskell wrapper to the SMTLIB-based- Horn-Clause/Logical Implication constraint solver used- for Liquid Types.- .- The solver itself is written in Ocaml.- .- The package includes:- .- 1. Types for Expressions, Predicates, Constraints, Solutions- .- 2. Code for serializing the above- .- 3. Code for parsing the results from the fixpoint.native binary- .- 4. The Ocaml fixpoint code and pre-compiled binaries- .- 5. (Deprecated) Z3 binaries if you want to link against the API.- .- Requirements- .- In addition to the .cabal dependencies you require- .- - A Z3 (<http://z3.codeplex.com>) or CVC4 (<http://cvc4.cs.nyu.edu>) binary.- If on Windows, please make sure to place the binary and any associated DLLs- in your "cabal/bin" folder, right next to the fixpoint.native.exe binary.- .- - An ocaml compiler (if installing with -fbuild-external).--Extra-Source-Files: configure- , external/fixpoint/Makefile- , external/fixpoint/*.ml- , external/fixpoint/smtZ3.mem.ml- , external/fixpoint/smtZ3.nomem.ml- , external/fixpoint/*.mli- , external/fixpoint/*.mll- , external/fixpoint/*.mly- , external/misc/*.ml- , external/misc/*.mli- , external/ocamlgraph/Makefile.in- , external/ocamlgraph/META.in- , external/ocamlgraph/configure- , external/ocamlgraph/configure.in- , external/ocamlgraph/lib/*.ml- , external/ocamlgraph/lib/*.mli- , external/ocamlgraph/src/*.ml- , external/ocamlgraph/src/*.mli- , external/ocamlgraph/src/*.mll- , external/ocamlgraph/src/*.mly- , external/z3/include/*.h- , external/z3/lib/libz3-a-32b- , external/z3/lib/libz3-a-64b- , external/z3/lib/libz3-so-32b- , external/z3/lib/libz3-so-64b- , external/z3/ocaml/build-lib.sh- , external/z3/ocaml/z3.ml- , external/z3/ocaml/*.c- , external/fixpoint/fixpoint.native-i386-linux- , external/fixpoint/fixpoint.native-i686-w64-mingw32- , external/fixpoint/fixpoint.native-x86_64-darwin- , external/fixpoint/fixpoint.native-x86_64-linux- , tests/neg/*.fq- , tests/pos/*.fq--Flag z3mem- Description: Link to Z3- Default: False--Flag build-external- Description: Build fixpoint.native binary from source (requires ocaml)- Default: False--Source-Repository head- Type: git- Location: https://github.com/ucsd-progsys/liquid-fixpoint/---- FIXME: This is a terrible hack. We build Fixpoint.hs *twice*, once--- targeting fixpoint.native so we can then *clobber* it with the--- OCaml fixpoint.native. This is required for cabal-install to detect--- fixpoint.native as an executable, and properly symlink it when--- asked.-Executable fixpoint.native- default-language: Haskell98- Main-is: Fixpoint.hs- Build-Depends: base >= 4.7 && < 5- , array- , syb- , cmdargs- , ansi-terminal- , bifunctors- , bytestring- , containers- , deepseq- , directory- , filepath- , mtl- , parsec- , pretty- , process- , syb- , text- , hashable- , unordered-containers- , text-format- , liquid-fixpoint---Executable fixpoint- default-language: Haskell98- Main-is: Fixpoint.hs- Build-Depends: base >= 4.7 && < 5- , array- , syb- , cmdargs- , ansi-terminal- , bifunctors- , bytestring- , containers- , deepseq- , directory- -- , filemanip- , filepath- , mtl- , parsec- , pretty- , process- , syb- , text- , hashable- , unordered-containers- , text-format- , liquid-fixpoint--Library- default-language: Haskell98- hs-source-dirs: src- Exposed-Modules: Language.Fixpoint.Names,- Language.Fixpoint.Files,- Language.Fixpoint.Errors,- Language.Fixpoint.Config,- Language.Fixpoint.Types,- Language.Fixpoint.Bitvector,- Language.Fixpoint.Visitor,- Language.Fixpoint.Sort,- Language.Fixpoint.Interface,- Language.Fixpoint.Parse,- Language.Fixpoint.PrettyPrint,- Language.Fixpoint.Smt.Types,- Language.Fixpoint.Smt.Theories,- Language.Fixpoint.Smt.Serialize,- Language.Fixpoint.Smt.Interface,- Language.Fixpoint.Misc,- Language.Fixpoint.Solver.Solution,- Language.Fixpoint.Solver.Worklist,- Language.Fixpoint.Solver.Monad,- Language.Fixpoint.Solver.Deps,- Language.Fixpoint.Solver.Uniqify,- Language.Fixpoint.Solver.Eliminate,- Language.Fixpoint.Solver.Validate,- Language.Fixpoint.Partition,- Language.Fixpoint.Statistics,- Language.Fixpoint.Solver.Solve-- Build-Depends: base >= 4.7 && < 5- , array- , attoparsec- , syb- , cmdargs- , ansi-terminal- , bifunctors- , bytestring- , containers- , deepseq- , directory- , filemanip- , filepath- , ghc-prim- , intern- , mtl- , parsec- , pretty- , process- , syb- , text- , transformers- , hashable- , unordered-containers- , text-format--test-suite test- default-language: Haskell98- type: exitcode-stdio-1.0- hs-source-dirs: tests- ghc-options: -O2 -threaded- main-is: test.hs- build-depends: base,- directory,- filepath,- process,- -- tagged,- liquid-fixpoint,- -- optparse-applicative == 0.11.*,- tasty >= 0.10,- -- tasty-quickcheck,- tasty-hunit,- tasty-rerun >= 1.1,- text+name: liquid-fixpoint +version: 0.4.0.0 +x-revision: 1 +Copyright: 2010-15 Ranjit Jhala, University of California, San Diego. +synopsis: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver +homepage: https://github.com/ucsd-progsys/liquid-fixpoint +license: BSD3 +license-file: LICENSE +author: Ranjit Jhala, Niki Vazou, Eric Seidel +maintainer: jhala@cs.ucsd.edu +category: Language +build-type: Custom +cabal-version: >=1.10 + +description: This package is a Haskell wrapper to the SMTLIB-based + Horn-Clause/Logical Implication constraint solver used + for Liquid Types. + . + The solver itself is written in Ocaml. + . + The package includes: + . + 1. Types for Expressions, Predicates, Constraints, Solutions + . + 2. Code for serializing the above + . + 3. Code for parsing the results from the fixpoint.native binary + . + 4. The Ocaml fixpoint code and pre-compiled binaries + . + 5. (Deprecated) Z3 binaries if you want to link against the API. + . + Requirements + . + In addition to the .cabal dependencies you require + . + - A Z3 (<http://z3.codeplex.com>) or CVC4 (<http://cvc4.cs.nyu.edu>) binary. + If on Windows, please make sure to place the binary and any associated DLLs + in your "cabal/bin" folder, right next to the fixpoint.native.exe binary. + . + - An ocaml compiler (if installing with -fbuild-external). + +Extra-Source-Files: configure + , external/fixpoint/Makefile + , external/fixpoint/*.ml + , external/fixpoint/smtZ3.mem.ml + , external/fixpoint/smtZ3.nomem.ml + , external/fixpoint/*.mli + , external/fixpoint/*.mll + , external/fixpoint/*.mly + , external/misc/*.ml + , external/misc/*.mli + , external/ocamlgraph/Makefile.in + , external/ocamlgraph/META.in + , external/ocamlgraph/configure + , external/ocamlgraph/configure.in + , external/ocamlgraph/lib/*.ml + , external/ocamlgraph/lib/*.mli + , external/ocamlgraph/src/*.ml + , external/ocamlgraph/src/*.mli + , external/ocamlgraph/src/*.mll + , external/ocamlgraph/src/*.mly + , external/z3/include/*.h + , external/z3/lib/libz3-a-32b + , external/z3/lib/libz3-a-64b + , external/z3/lib/libz3-so-32b + , external/z3/lib/libz3-so-64b + , external/z3/ocaml/build-lib.sh + , external/z3/ocaml/z3.ml + , external/z3/ocaml/*.c + , external/fixpoint/fixpoint.native-i386-linux + , external/fixpoint/fixpoint.native-i686-w64-mingw32 + , external/fixpoint/fixpoint.native-x86_64-darwin + , external/fixpoint/fixpoint.native-x86_64-linux + , tests/neg/*.fq + , tests/pos/*.fq + +Flag z3mem + Description: Link to Z3 + Default: False + +Flag build-external + Description: Build fixpoint.native binary from source (requires ocaml) + Default: False + +Source-Repository head + Type: git + Location: https://github.com/ucsd-progsys/liquid-fixpoint/ + +-- FIXME: This is a terrible hack. We build Fixpoint.hs *twice*, once +-- targeting fixpoint.native so we can then *clobber* it with the +-- OCaml fixpoint.native. This is required for cabal-install to detect +-- fixpoint.native as an executable, and properly symlink it when +-- asked. +Executable fixpoint.native + default-language: Haskell98 + Main-is: Fixpoint.hs + Build-Depends: base >= 4.6 && < 5 + , array + , syb + , cmdargs + , ansi-terminal + , bifunctors + , bytestring + , containers + , deepseq + , directory + , filepath + , mtl + , parsec + , pretty + , process + , syb + , text + , hashable + , unordered-containers + , text-format + , liquid-fixpoint + + +Executable fixpoint + default-language: Haskell98 + Main-is: Fixpoint.hs + Build-Depends: base >= 4.6 && < 5 + , array + , syb + , cmdargs + , ansi-terminal + , bifunctors + , bytestring + , containers + , deepseq + , directory + -- , filemanip + , filepath + , mtl + , parsec + , pretty + , process + , syb + , text + , hashable + , unordered-containers + , text-format + , liquid-fixpoint + +Library + default-language: Haskell98 + hs-source-dirs: src + Exposed-Modules: Language.Fixpoint.Names, + Language.Fixpoint.Files, + Language.Fixpoint.Errors, + Language.Fixpoint.Config, + Language.Fixpoint.Types, + Language.Fixpoint.Bitvector, + Language.Fixpoint.Visitor, + Language.Fixpoint.Sort, + Language.Fixpoint.Interface, + Language.Fixpoint.Parse, + Language.Fixpoint.PrettyPrint, + Language.Fixpoint.Smt.Types, + Language.Fixpoint.Smt.Theories, + Language.Fixpoint.Smt.Serialize, + Language.Fixpoint.Smt.Interface, + Language.Fixpoint.Misc, + Language.Fixpoint.Solver.Solution, + Language.Fixpoint.Solver.Worklist, + Language.Fixpoint.Solver.Monad, + Language.Fixpoint.Solver.Deps, + Language.Fixpoint.Solver.Uniqify, + Language.Fixpoint.Solver.Eliminate, + Language.Fixpoint.Solver.Validate, + Language.Fixpoint.Partition, + Language.Fixpoint.Statistics, + Language.Fixpoint.Solver.Solve + + Build-Depends: base >= 4.6 && < 5 + , array + , attoparsec + , syb + , cmdargs + , ansi-terminal + , bifunctors + , bytestring + , containers + , deepseq + , directory + , filemanip + , filepath + , ghc-prim + , intern + , mtl + , parsec + , pretty + , process + , syb + , text + , transformers + , hashable + , unordered-containers + , text-format + +test-suite test + default-language: Haskell98 + type: exitcode-stdio-1.0 + hs-source-dirs: tests + ghc-options: -O2 -threaded + main-is: test.hs + build-depends: base, + directory, + filepath, + process, + -- tagged, + liquid-fixpoint, + -- optparse-applicative == 0.11.*, + tasty >= 0.10, + -- tasty-quickcheck, + tasty-hunit, + tasty-rerun >= 1.1, + text
revision 2
name: liquid-fixpoint version: 0.4.0.0 -x-revision: 1 +x-revision: 2 Copyright: 2010-15 Ranjit Jhala, University of California, San Diego. synopsis: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver homepage: https://github.com/ucsd-progsys/liquid-fixpoint Executable fixpoint.native default-language: Haskell98 Main-is: Fixpoint.hs - Build-Depends: base >= 4.6 && < 5 + Build-Depends: base >= 4.7 && < 5 , array , syb , cmdargs Executable fixpoint default-language: Haskell98 Main-is: Fixpoint.hs - Build-Depends: base >= 4.6 && < 5 + Build-Depends: base >= 4.7 && < 5 , array , syb , cmdargs Language.Fixpoint.Statistics, Language.Fixpoint.Solver.Solve - Build-Depends: base >= 4.6 && < 5 + Build-Depends: base >= 4.7 && < 5 , array , attoparsec , syb