Cabal revisions of containers-verified-0.5.11.0
Hackage metadata revisions edit the .cabal file after upload; each diff below is one revision.
revision 1
-name: containers-verified-version: 0.5.11.0-synopsis: Formally verified drop-in replacement of containers-description:- In the context of the <https://deepspec.org/main DeepSpec project>, parts of the- <http://hackage.haskell.org/package/containers containers> library were- formally verified using <https://github.com/antalsz/hs-to-coq hs-to-coq> and- the interactive theorem prover Coq.- .- This package depends on precisely the verified version of containers and- re-exports the verified parts of the API, with module name and function name- unchanged.- .- If you happen to use only the verified subset of the API, then you can simply change- @containers@ to @containers-verified@ in your @.cabal@ file and earn bragging- rights about using verified data structures in your project. Because the- types from @containers@ are re-exported, you can still interface with other- libraries that depend on @containers@ directly.- .- If you happen to need additional modules or functions, you will have to- depend on both @containers@ and @containers-verified@, and use- <https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#package-qualified-imports package-qualified imports> to disambiguate.- .- This package does not re-export any of the @….Internals@ modules.- .- We cannot control which type class instances are re-exported; these therefore- may give you access to unverified code. Also, the @conatiners@ code contains- some CPP directives; these can enable different code on your machine than the- code that we verified (e.g. different bit-widths).- .- To learn more about what exactly has been verified, and how wide the- formalization gap is, see the paper “Ready, Set, Verify! Applying hs-to-coq- to non-trivial Haskell code” by Joachim Breitner, Antal Spector-Zabusky, Yao- Li, Christine Rizkallah, John Wiegley and Stephanie Weirich.-- .- The long-term maintenance plan for this package is not fleshed out yet, and- certainly depends on user-demand. Let us know your needs! (And your- technical or financial abilities to contribute...)---homepage: https://github.com/nomeata/containers-verified-license: MIT-license-file: LICENSE-author: Joachim Breitner-maintainer: mail@joachim-breitner.de-copyright: 2018 Joachim Breitner-category: Data-build-type: Simple-extra-source-files: ChangeLog.md-cabal-version: >=1.10--library- build-depends: containers ==0.5.11.0- default-language: Haskell2010- exposed-modules:- Data.Set- Data.IntSet- Data.Map--source-repository head- type: git- location: http://github.com/nomeata/containers-verified-+name: containers-verified +version: 0.5.11.0 +x-revision: 1 +synopsis: Formally verified drop-in replacement of containers +description: + In the context of the <https://deepspec.org/main DeepSpec project>, parts of the + <http://hackage.haskell.org/package/containers containers> library were + formally verified using <https://github.com/antalsz/hs-to-coq hs-to-coq> and + the interactive theorem prover Coq. + . + This package depends on precisely the verified version of containers and + re-exports the verified parts of the API, with module name and function name + unchanged. + . + If you happen to use only the verified subset of the API, then you can simply change + @containers@ to @containers-verified@ in your @.cabal@ file and earn bragging + rights about using verified data structures in your project. Because the + types from @containers@ are re-exported, you can still interface with other + libraries that depend on @containers@ directly. + . + If you happen to need additional modules or functions, you will have to + depend on both @containers@ and @containers-verified@, and use + <https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#package-qualified-imports package-qualified imports> to disambiguate. + . + This package does not re-export any of the @….Internals@ modules. + . + We cannot control which type class instances are re-exported; these therefore + may give you access to unverified code. Also, the @conatiners@ code contains + some CPP directives; these can enable different code on your machine than the + code that we verified (e.g. different bit-widths). + . + To learn more about what exactly has been verified, and how wide the + formalization gap is, see the paper “Ready, Set, Verify! Applying hs-to-coq + to real-world Haskell code” by Joachim Breitner, Antal Spector-Zabusky, Yao + Li, Christine Rizkallah, John Wiegley and Stephanie Weirich. + + . + The long-term maintenance plan for this package is not fleshed out yet, and + certainly depends on user-demand. Let us know your needs! (And your + technical or financial abilities to contribute...) + + +homepage: https://github.com/nomeata/containers-verified +license: MIT +license-file: LICENSE +author: Joachim Breitner +maintainer: mail@joachim-breitner.de +copyright: 2018 Joachim Breitner +category: Data +build-type: Simple +extra-source-files: ChangeLog.md +cabal-version: >=1.10 + +library + build-depends: containers ==0.5.11.0 + default-language: Haskell2010 + exposed-modules: + Data.Set + Data.IntSet + Data.Map + +source-repository head + type: git + location: http://github.com/nomeata/containers-verified +
revision 2
name: containers-verified version: 0.5.11.0 -x-revision: 1 +x-revision: 2 synopsis: Formally verified drop-in replacement of containers description: In the context of the <https://deepspec.org/main DeepSpec project>, parts of the code that we verified (e.g. different bit-widths). . To learn more about what exactly has been verified, and how wide the - formalization gap is, see the paper “Ready, Set, Verify! Applying hs-to-coq - to real-world Haskell code” by Joachim Breitner, Antal Spector-Zabusky, Yao + formalization gap is, see the paper <https://arxiv.org/abs/1803.06960 “Ready, Set, Verify! Applying hs-to-coq + to real-world Haskell code”> by Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley and Stephanie Weirich. .
revision 3
name: containers-verified version: 0.5.11.0 -x-revision: 2 +x-revision: 3 synopsis: Formally verified drop-in replacement of containers description: In the context of the <https://deepspec.org/main DeepSpec project>, parts of the code that we verified (e.g. different bit-widths). . To learn more about what exactly has been verified, and how wide the - formalization gap is, see the paper <https://arxiv.org/abs/1803.06960 “Ready, Set, Verify! Applying hs-to-coq - to real-world Haskell code”> by Joachim Breitner, Antal Spector-Zabusky, Yao - Li, Christine Rizkallah, John Wiegley and Stephanie Weirich. + formalization gap is, see the paper + <https://arxiv.org/abs/1803.06960 “Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code”> + by Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley and Stephanie Weirich. . The long-term maintenance plan for this package is not fleshed out yet, and