GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-11 14:06:13 +03:00
Code Issues Projects Releases Wiki Activity
WIP/rpc/feat/newtype
cryptol/cryptol.cabal

291 lines
11 KiB
Plaintext
Raw Permalink Normal View History

Update cabal file to include all relevant files in the `lib` directory.
2020-10-28 03:40:39 +03:00
Cabal-version: 2.4
it's not just a parser anymore
2014-04-18 21:18:26 +04:00
Name: cryptol
Bump version after release (#1148)
2021-04-05 19:52:25 +03:00
Version: 2.11.0.99
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Synopsis: Cryptol: The Language of Cryptography
clean up cabal file for Hackagability Fixes #18
2015-03-10 01:16:53 +03:00
Description: Cryptol is a domain-specific language for specifying cryptographic algorithms. A Cryptol implementation of an algorithm resembles its mathematical specification more closely than an implementation in a general purpose language. For more, see <http://www.cryptol.net/>.
Update cabal file to include all relevant files in the `lib` directory.
2020-10-28 03:40:39 +03:00
License: BSD-3-Clause
Allow use of Cabal 1.18 during build This eases the build using Stack and GHC 7.8, since GHC 7.8 comes with Cabal 1.18.
2015-06-26 23:45:26 +03:00
License-file: LICENSE
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Author: Galois, Inc.
Maintainer: cryptol@galois.com
clean up cabal file for Hackagability Fixes #18
2015-03-10 01:16:53 +03:00
Homepage: http://www.cryptol.net/
Bug-reports: https://github.com/GaloisInc/cryptol/issues
Tweak a few things for 2.9.0 (#833) * Fix Dockerfile * Include version number in CHANGES.md * Update copyright dates * Don't include cryptol-specs in release archives * Remove duplicate copy of Programming Cryptol
2020-07-28 18:41:27 +03:00
Copyright: 2013-2020 Galois Inc.
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Category: Language
switch to TH solution for GitRev This helps with #18 and should also reduce the number of unnecessary recompiles that were triggered by the Makefile and/or cabal. The cabal build type is now Simple. Most of the complication in the TH.hs module is due to the various places the current git hash might be stored: 1. Detached HEAD: the hash is in `.git/HEAD` 2. On a branch or tag: the hash is in a file pointed to by `.git/HEAD` in a location like `.git/refs/heads` 3. On a branch or tag but in a repository with packed refs: the hash is in `.git/packed-refs` These situations all arise under normal development workflows and on the Jenkins build machines, but there might be further scenarios that cause problems. The tradeoff seems worthwhile though as now projects that build Cryptol as a dependency wind up having to rebuild Cryptol far less frequently.
2015-03-16 23:18:28 +03:00
Build-type: Simple
Put bench/data/*.cry in extra-source-files
2016-05-20 22:04:53 +03:00
extra-source-files: bench/data/*.cry
Add CHANGES.md file
2019-04-30 02:17:54 +03:00
CHANGES.md
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Update cabal file to include all relevant files in the `lib` directory.
2020-10-28 03:40:39 +03:00
data-files: **/*.cry **/*.z3
Fixes #172 There's now a more sensible hierarchy of locations that Cryptol uses to look for modules. By default, in order it looks for libraries in: 1. The directories specified in the CRYPTOLPATH environment variable 2. The current directory 3. The user data directory (something like `$HOME/.cryptol`) 4. Relative to the executable's install directory 5. The static path used when building the executable (cabal's data-dir) There is also a new command-line flag for the interpreter: `--cryptolpath-only` which makes the interpreter ignore locations 2-5. This commit also reworks the Makefile and build/release process. These are bunched together because they play off each other quite a bit; the build/release process determines the location of the `Cryptol.cry`, which must be found when looking for modules. Rather than leaning on `cabal install`, we now use a combination of `cabal configure`, `cabal build`, and `cabal copy`. A couple of upshots to this: - More of the release staging is handled by cabal -- we don't have to go in and manually copy things out of the sandbox. In fact, the `cryptol` executable never goes into the sandbox. - The testing infrastructure runs on executables that are in place in the staging directory, rather than in the sandbox. This should be more hygienic and realistic. - The `Cryptol.cry` prelude file is now in `/share/cryptol` in order to better reflect the common POSIX structure. This means Cryptol will play nicer in global installs, and mirrors what other interpreted languages do. - The default build settings use a prefix of `/usr/local` rather than using the sandbox directory. This makes them more relocatable for binary distributions. Set PREFIX= before making to change this.
2015-01-22 02:03:16 +03:00
data-dir: lib
Initial import from internal repo
2014-04-18 02:34:25 +04:00
clean up cabal file for Hackagability Fixes #18
2015-03-10 01:16:53 +03:00
source-repository head
type: git
location: https://github.com/GaloisInc/cryptol.git
source-repository this
type: git
location: https://github.com/GaloisInc/cryptol.git
Fix some cabal warnings and such
2020-11-10 20:36:05 +03:00
-- add a tag on release branches
-- tag:
Initial import from internal repo
2014-04-18 02:34:25 +04:00
flag static
default: False
description: Create a statically-linked binary
distribution tweaks Makefile now has two modes depending on whether PREFIX is set. If it's not, we try to make the distribution as relocatable as possible, meaning we don't rely on the baked-in-by-cabal data directory. If it is set, we do use that path.
2015-03-04 03:22:14 +03:00
flag relocatable
default: True
description: Don't use the Cabal-provided data directory for looking up Cryptol libraries. This is useful when the data directory can't be known ahead of time, like for a relocatable distribution.
Initial import from internal repo
2014-04-18 02:34:25 +04:00
library
Add default-language to cabal file. Closes #71
2014-09-15 01:37:37 +04:00
Default-language:
Bump language standard to 2010. We're beyond '98 anyway...
2017-10-24 21:59:34 +03:00
Haskell2010
clean up 7.8-isms
2016-06-07 23:40:15 +03:00
Build-depends: base >= 4.8 && < 5,
Add `any` solver support to the What4 backend. This turned out to be relatively straightforward. Using a simliar strategy to SBV, we simply spawn off all the solvers in separate threads and wait using the `async` package. Some minor fixes in `What4` allow the threads to respond properly to being interrupted. Some care is required to install the necessary solver options _before_ spawning off the threads to avoid race conditions in the configuration datastructure itself; such race conditions should be fixed in What4 at some point.
2020-06-30 20:09:49 +03:00
async >= 2.2 && < 2.3,
Bump base-compat upper bound.
2020-03-01 09:12:39 +03:00
base-compat >= 0.6 && < 0.12,
update to bv-sized branch of what4
2020-05-06 23:01:57 +03:00
bv-sized >= 1.0 && < 1.1,
Merge branch 'master' into writeFile
2015-12-26 08:39:01 +03:00
bytestring >= 0.10,
start improving handling of interrupts in server This notably adds a `MonadBaseControl` instance for the `REPL` monad so that we can catch asynchronous exceptions in the middle of `REPL` computations. Since this is a generalization of Haskeline's exception support, that orphan instance for the console executable is now in terms of this new instance.
2015-12-04 02:36:43 +03:00
array >= 0.4,
containers >= 0.5,
Track file content fingerprints alongside loaded modules
2019-02-28 01:37:39 +03:00
cryptohash-sha1 >= 0.11 && < 0.12,
start improving handling of interrupts in server This notably adds a `MonadBaseControl` instance for the `REPL` monad so that we can catch asynchronous exceptions in the middle of `REPL` computations. Since this is a generalization of Haskeline's exception support, that orphan instance for the console executable is now in terms of this new instance.
2015-12-04 02:36:43 +03:00
deepseq >= 1.3,
clean up 7.8-isms
2016-06-07 23:40:15 +03:00
directory >= 1.2.2.0,
Updates for haskeline 0.8 and use of exceptions package.
2020-05-07 00:14:47 +03:00
exceptions,
start improving handling of interrupts in server This notably adds a `MonadBaseControl` instance for the `REPL` monad so that we can catch asynchronous exceptions in the middle of `REPL` computations. Since this is a generalization of Haskeline's exception support, that orphan instance for the console executable is now in terms of this new instance.
2015-12-04 02:36:43 +03:00
filepath >= 1.3,
gitrev >= 1.0,
Perform internal modular arithmetic on the `BigNat` type instead of `Integer`. This resuts in a modest reduction in runtime.
2020-09-24 22:50:37 +03:00
ghc-prim,
start improving handling of interrupts in server This notably adds a `MonadBaseControl` instance for the `REPL` monad so that we can catch asynchronous exceptions in the middle of `REPL` computations. Since this is a generalization of Haskeline's exception support, that orphan instance for the console executable is now in terms of this new instance.
2015-12-04 02:36:43 +03:00
GraphSCC >= 1.0.4,
heredoc >= 0.2,
Rely on `integer-gmp` primitives for primality tests and modular inverse computations instead of using the arithmoi and semiring packages.
2020-09-29 21:23:23 +03:00
integer-gmp >= 1.0 && < 1.1,
Update to use `libBF` version 0.6, which has some bugfixes and additional operations.
2021-01-29 02:24:15 +03:00
libBF >= 0.6 && < 0.7,
Add basic support for primality checking in the type system.
2020-05-19 01:42:17 +03:00
MemoTrie >= 0.6 && < 0.7,
start improving handling of interrupts in server This notably adds a `MonadBaseControl` instance for the `REPL` monad so that we can catch asynchronous exceptions in the middle of `REPL` computations. Since this is a generalization of Haskeline's exception support, that orphan instance for the console executable is now in terms of this new instance.
2015-12-04 02:36:43 +03:00
monad-control >= 1.0,
monadLib >= 3.7.2,
Very basic scaffolding for using what4 as a symbolic backend
2020-03-03 21:00:51 +03:00
parameterized-utils >= 2.0.2,
start improving handling of interrupts in server This notably adds a `MonadBaseControl` instance for the `REPL` monad so that we can catch asynchronous exceptions in the middle of `REPL` computations. Since this is a generalization of Haskeline's exception support, that orphan instance for the console executable is now in terms of this new instance.
2015-12-04 02:36:43 +03:00
pretty >= 1.1,
process >= 1.2,
Allow sbv 8.14 Tested to build fine here.
2021-04-13 22:33:21 +03:00
sbv >= 8.6 && < 8.15,
Bump simple-smt version bounds to pull in a bug fix. Fixes #457
2017-10-03 20:20:15 +03:00
simple-smt >= 0.7.1,
Rework the thunk lifecycle to remove race conditions. Thunk state is now controlled using transational memory variables instead of IORefs, and the thunk likecycle is made more explicit in the relevant datatypes. Threads will now properly block and wait when forcing a thunk that is already under evaluation by a different thread. Hopefully, using optimistic concurrency (transactional memory) will help reduce concurrency contention. The reworked lifecycle datastructures hopefully will release closures related to evaluation faster, which should reduce memory pressure somewhat. Fixes #856
2020-08-21 19:02:37 +03:00
stm >= 2.4,
Fix spurious failures due to lazy I/O Regression test check31 was failing somewhat unpredictably due to the use of lazy I/O when loading the Z3 prelude for the type checker. Using the `strict` package seems to fix it.
2017-09-14 01:31:43 +03:00
strict,
start improving handling of interrupts in server This notably adds a `MonadBaseControl` instance for the `REPL` monad so that we can catch asynchronous exceptions in the middle of `REPL` computations. Since this is a generalization of Haskeline's exception support, that orphan instance for the console executable is now in terms of this new instance.
2015-12-04 02:36:43 +03:00
text >= 1.1,
tf-random >= 0.5,
transformers-base >= 0.4,
Modifications to make cryptol compile with SBV 7.0 Also, bumped up the version to 2.4.1
2017-07-18 20:25:00 +03:00
mtl >= 2.2.1,
Very basic scaffolding for using what4 as a symbolic backend
2020-03-03 21:00:51 +03:00
time >= 1.6.0.1,
panic >= 0.3,
Convert to using the `SFloat` module from What4. Expose some additional primitives, such as FMA, abs, sqrt, and more classification predicates. Refactor the primitives table for floating-point values into a single generic table that uses methods from the `Backend` class.
2021-02-09 04:47:49 +03:00
what4 >= 1.1 && < 1.2
Delete old solver stuff. The main user visible effect of this might be that sometime things on the Cryptol command line are instantiated in a slightly different way: we get `inf` sometimes when we got a finite example before. We could work around this if it is an issue, but I am not sure which behavior is more reasonable.
2017-09-27 00:02:52 +03:00
Fix some cabal warnings and such
2020-11-10 20:36:05 +03:00
Build-tool-depends: alex:alex, happy:happy
Remove custom fork of SBV library in favor of the official SBV-4.0. Fixes #35.
2015-01-24 01:22:18 +03:00
hs-source-dirs: src
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Rename module `Cryptol.Prims.Eval` into `Cryptol.Eval.Concrete`. This fits better into the current module structure, and is a lot less confusing.
2020-03-09 21:29:08 +03:00
Exposed-modules: Cryptol.Parser,
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Cryptol.Parser.Lexer,
Cryptol.Parser.AST,
Cryptol.Parser.Position,
Cryptol.Parser.Names,
Major changes plumbed through, now for the bugs!
2015-09-25 00:47:52 +03:00
Cryptol.Parser.Name,
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Cryptol.Parser.NoPat,
Cryptol.Parser.NoInclude,
Split new modules Fixity and Selector from Cryptol.Parser.AST.
2018-06-12 00:28:49 +03:00
Cryptol.Parser.Selector,
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Cryptol.Parser.Utils,
Cryptol.Parser.Unlit,
Refactor Fixity module so Cryptol.Utils.PP can import it. Also make some other parts of the code less dependent on the internal representation of the Fixity datatype.
2019-12-14 09:41:55 +03:00
Cryptol.Utils.Fixity,
Major changes plumbed through, now for the bugs!
2015-09-25 00:47:52 +03:00
Cryptol.Utils.Ident,
Implement and use a new RecordMap type. This type stores records as a finite map from field names to values, while also remembering the original order of the fields from when the record was generated (usually, from the program source). For all "semantic" purposes, the fields are treated as appearing in a canoical order (in sorted order of the field names). However, for user display purposes, records are presented in the order in which the fields were originally stated. In the course of implementing this, I discovered that we were not previously checking for repeated fields in the parser or typechecker, which would result in some rather strange situations and could probably be used to break the type safety. This is now fixed and repeated fields will result in either a parse error or a panic (for records generated internally). Fixes #706
2020-06-27 02:37:54 +03:00
Cryptol.Utils.RecordMap,
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Cryptol.Utils.PP,
Cryptol.Utils.Panic,
Cryptol.Utils.Debug,
Make general substitutions, and move code into AST module.
2014-12-05 22:46:09 +03:00
Cryptol.Utils.Misc,
More rules and things; external solver disabled; we can at least load ChaCha
2017-02-09 02:08:50 +03:00
Cryptol.Utils.Patterns,
Don't print directly to stdout. Fixes #166
2017-10-05 01:50:31 +03:00
Cryptol.Utils.Logger,
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Cryptol.Version,
Cryptol.ModuleSystem,
Cryptol.ModuleSystem.Base,
Cryptol.ModuleSystem.Env,
Track file content fingerprints alongside loaded modules
2019-02-28 01:37:39 +03:00
Cryptol.ModuleSystem.Fingerprint,
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Cryptol.ModuleSystem.Interface,
Cryptol.ModuleSystem.Monad,
Add a naming environment to the pretty printer
2015-05-21 23:42:54 +03:00
Cryptol.ModuleSystem.Name,
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Cryptol.ModuleSystem.NamingEnv,
Split out exports specs; add some parsing for functor instances.
2017-10-03 01:01:45 +03:00
Cryptol.ModuleSystem.Exports,
Basics of sort of module instantiation
2017-09-30 02:27:13 +03:00
Cryptol.ModuleSystem.InstantiateModule,
Implementation of nested modules. * Limitations: Does not work in combination parameterized modules, as I am about to redo how that works. * General refeactorings: * Namespaces: - We have an explicit type for namespaces, see `Cryptol.Util.Ident` - Display environments should now be aware of the namespace of the name being displayed. * Renamer: - Factor out the renamer monad and error type into separate modules - All name resultion is done through a single function `resolveName` - The renamer now computes the dependencies between declarations, orders things in dependency order, and checks for bad recursion. * Typechecker: Redo checking of declarations (both top-level and local). Previously we used a sort of CPS to add things in scope. Now we use a state monad and add things to the state. We assume that the renamer has been run, which means that declarations are ordered in dependency order, and things have unique name, so we don't need to worry about scoping too much. * Change specific to nested modules: - We have a new namespace for module names - The interface file of a module contains the interfaces for nested modules - Most of the changes related to nested modules in the renamer are in `ModuleSystem.NamingEnv` and `ModuleSystem.Rename` - There is some trickiness when resolving module names when importing submodules (seed `processOpen` and `openLoop`) - There are some changes to the representation of modules in the typechecked syntax, in particular: - During type-checking we "flatten" nested module declarations into a single big declaration. Hopefully, this means that passes after the type checker don't need to worry about nested modules - There is a new field containing the interfaces of the nested modules, this is needed so that when we import the module we know we have the nested structure - Declarations in functor/parameterzied modules do not appear in the flattened list of declarations. Instead thouse modules are collected in a separate field, and the plan is that they would be used from there when we implmenet functor instantiation.
2021-01-27 02:54:24 +03:00
Cryptol.ModuleSystem.Renamer,
Cryptol.ModuleSystem.Renamer.Monad,
Cryptol.ModuleSystem.Renamer.Error,
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Cryptol.TypeCheck,
Checkpoint.
2017-01-31 05:14:10 +03:00
Cryptol.TypeCheck.Type,
Move type-level primitives to the Prelude. For the time being, there is still some information about them that is duplicated in Cryptol.TypeCheck.TCon, but we at least the parsed syntax does not depend on the typechecked syntax.
2019-07-03 03:34:36 +03:00
Cryptol.TypeCheck.TCon,
More rules and things; external solver disabled; we can at least load ChaCha
2017-02-09 02:08:50 +03:00
Cryptol.TypeCheck.TypePat,
Cryptol.TypeCheck.SimpType,
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Cryptol.TypeCheck.AST,
more polished
2017-08-15 01:45:37 +03:00
Cryptol.TypeCheck.Parseable,
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Cryptol.TypeCheck.Monad,
Cryptol.TypeCheck.Infer,
Merge branch 'abstract-types' of github.com:GaloisInc/cryptol into abstract-types # Conflicts: # src/Cryptol/ModuleSystem/InstantiateModule.hs
2017-10-05 22:45:11 +03:00
Cryptol.TypeCheck.CheckModuleInstance,
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Cryptol.TypeCheck.InferTypes,
Implementation of nested modules. * Limitations: Does not work in combination parameterized modules, as I am about to redo how that works. * General refeactorings: * Namespaces: - We have an explicit type for namespaces, see `Cryptol.Util.Ident` - Display environments should now be aware of the namespace of the name being displayed. * Renamer: - Factor out the renamer monad and error type into separate modules - All name resultion is done through a single function `resolveName` - The renamer now computes the dependencies between declarations, orders things in dependency order, and checks for bad recursion. * Typechecker: Redo checking of declarations (both top-level and local). Previously we used a sort of CPS to add things in scope. Now we use a state monad and add things to the state. We assume that the renamer has been run, which means that declarations are ordered in dependency order, and things have unique name, so we don't need to worry about scoping too much. * Change specific to nested modules: - We have a new namespace for module names - The interface file of a module contains the interfaces for nested modules - Most of the changes related to nested modules in the renamer are in `ModuleSystem.NamingEnv` and `ModuleSystem.Rename` - There is some trickiness when resolving module names when importing submodules (seed `processOpen` and `openLoop`) - There are some changes to the representation of modules in the typechecked syntax, in particular: - During type-checking we "flatten" nested module declarations into a single big declaration. Hopefully, this means that passes after the type checker don't need to worry about nested modules - There is a new field containing the interfaces of the nested modules, this is needed so that when we import the module we know we have the nested structure - Declarations in functor/parameterzied modules do not appear in the flattened list of declarations. Instead thouse modules are collected in a separate field, and the plan is that they would be used from there when we implmenet functor instantiation.
2021-01-27 02:54:24 +03:00
Cryptol.TypeCheck.Interface,
Move errors to their own module.
2017-12-22 00:59:43 +03:00
Cryptol.TypeCheck.Error,
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Cryptol.TypeCheck.Kind,
Cryptol.TypeCheck.Subst,
Cryptol.TypeCheck.Instantiate,
Cryptol.TypeCheck.Unify,
Cryptol.TypeCheck.PP,
Cryptol.TypeCheck.Solve,
Move defaulting code to a separate module.
2017-12-23 03:01:19 +03:00
Cryptol.TypeCheck.Default,
Checkpoint.
2017-01-31 05:14:10 +03:00
Cryptol.TypeCheck.SimpleSolver,
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Cryptol.TypeCheck.TypeMap,
New module Cryptol.TypeCheck.TypeOf has functions to compute Type of an Expr
2014-05-10 03:27:07 +04:00
Cryptol.TypeCheck.TypeOf,
First stab at type-checker sanity checking.
2015-05-20 00:25:56 +03:00
Cryptol.TypeCheck.Sanity,
Initial import from internal repo
2014-04-18 02:34:25 +04:00
More aggressive goal simplification.
2017-02-01 01:12:53 +03:00
Cryptol.TypeCheck.Solver.Types,
Redo the export to SMT story in a much simpler way.
2017-02-17 03:46:38 +03:00
Cryptol.TypeCheck.Solver.SMT,
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Cryptol.TypeCheck.Solver.InfNat,
Cryptol.TypeCheck.Solver.Class,
Cryptol.TypeCheck.Solver.Selector,
Cryptol.TypeCheck.Solver.Utils,
Checkpoint.
2017-01-31 05:14:10 +03:00
Cryptol.TypeCheck.Solver.Numeric,
More rules and things; external solver disabled; we can at least load ChaCha
2017-02-09 02:08:50 +03:00
Cryptol.TypeCheck.Solver.Improve,
Improvement improvements Integrate interval analysis into improvements to simplify fin constraints, and rewriting of equality constraints.
2015-08-15 03:38:41 +03:00
Cryptol.TypeCheck.Solver.Numeric.Fin,
Cryptol.TypeCheck.Solver.Numeric.Interval,
Split-up `CrySat` into multiple modules.
2014-12-02 03:28:29 +03:00
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Cryptol.Transform.MonoValues,
Cryptol.Transform.Specialize,
Add a pass to rewrite a param. module, into a non-param module All definitions are parameterized by all parameters.
2017-10-19 23:45:40 +03:00
Cryptol.Transform.AddModParams,
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Allow evaluation in parameterized module, as long as parameters are not used.
2017-10-28 00:59:32 +03:00
Cryptol.IR.FreeVars,
Code motion and renaming related to the bulk file move that created the `Backend` module tree. The main change here is that the `Cryptol.Eval.SBV` module was split into two, similar to how the concrete and What4 evaluators were already split. Various other small bits of code are rearranged to detangle module dependencies.
2020-10-09 03:33:20 +03:00
Cryptol.Backend,
Also move the Cryptol.Eval.Arch module under the Backend tree
2020-10-09 03:43:19 +03:00
Cryptol.Backend.Arch,
Code motion and renaming related to the bulk file move that created the `Backend` module tree. The main change here is that the `Cryptol.Eval.SBV` module was split into two, similar to how the concrete and What4 evaluators were already split. Various other small bits of code are rearranged to detangle module dependencies.
2020-10-09 03:33:20 +03:00
Cryptol.Backend.Concrete,
Cryptol.Backend.FloatHelpers,
Cryptol.Backend.Monad,
Break `SeqMap` out into a separate module
2021-03-26 07:39:35 +03:00
Cryptol.Backend.SeqMap,
Code motion and renaming related to the bulk file move that created the `Backend` module tree. The main change here is that the `Cryptol.Eval.SBV` module was split into two, similar to how the concrete and What4 evaluators were already split. Various other small bits of code are rearranged to detangle module dependencies.
2020-10-09 03:33:20 +03:00
Cryptol.Backend.SBV,
Cryptol.Backend.What4,
Move `WordValue` into a separate module.
2021-03-26 22:06:26 +03:00
Cryptol.Backend.WordValue,
Code motion and renaming related to the bulk file move that created the `Backend` module tree. The main change here is that the `Cryptol.Eval.SBV` module was split into two, similar to how the concrete and What4 evaluators were already split. Various other small bits of code are rearranged to detangle module dependencies.
2020-10-09 03:33:20 +03:00
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Cryptol.Eval,
Rename module `Cryptol.Prims.Eval` into `Cryptol.Eval.Concrete`. This fits better into the current module structure, and is a lot less confusing.
2020-03-09 21:29:08 +03:00
Cryptol.Eval.Concrete,
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Cryptol.Eval.Env,
Split out the primitive definitions used by multiple evalautors into a `Generic` module. Refactor the `EvalPrims` class away, pusing the `iteValue` operation into `BitWord` and demoting the `evalPrim` operation into an ordinary (non-typeclass) operation.
2020-03-10 00:09:19 +03:00
Cryptol.Eval.Generic,
Refactor how primitives are represented. We invent a lightweight syntax for primitives that is evaluated to values when a primitive is looked up at evaluation time. Currently, this does not add any additional capabilities, but gives us the ability to modify the representation of values without touching all the primitive definitions, and gives us a place to hook in additional capabilies to the primitives. As part of this refactoring, the primitives that are defined totally generically are moved to the `Cryptol.Eval.Generic` module and used uniformly in all the backends.
2020-11-24 21:02:59 +03:00
Cryptol.Eval.Prims,
Add new unoptimized reference interpreter; use in REPL with ":eval <expr>"
2017-02-03 20:02:25 +03:00
Cryptol.Eval.Reference,
Refactor `Cryptol.Symbolic.Prims` and `Cryptol.Symbolic.Value` into a single new module `Crypol.Eval.SBV`.
2020-03-10 00:32:07 +03:00
Cryptol.Eval.SBV,
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Cryptol.Eval.Type,
Cryptol.Eval.Value,
Very basic scaffolding for using what4 as a symbolic backend
2020-03-03 21:00:51 +03:00
Cryptol.Eval.What4,
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Add a basic implementation of AES to the SuiteB module. This implementation is taken fairly directly from the SBV tutorial module. It is a Word32-oriented implementation using TBoxes. We make the implementation avalible via Cryptol primitives that are similar to the AESNI instructions, with primitives for the individual rounds and some utility primitives for performing key expansion.
2020-09-15 04:35:29 +03:00
Cryptol.AES,
Add faster primitive implementations for `pmult`, `pdiv`, and `pmod`.
2020-10-01 21:37:21 +03:00
Cryptol.F2,
Add a Haskell-native implementation of the SHA256 and SHA512 block functions, ripped out of the SHA package, and expose it via new Cryptol primitives. Using these primitives in place of the defined reference implementations leads to approx 100x speed-up in larger protocols that do a lot of hashing. I don't know if this is the implementation we'll actually end up using, but this verifies the overall idea and helps design the API.
2020-09-04 19:03:58 +03:00
Cryptol.SHA,
Add a new built-in module for prime-field eliptic curves, based on the arithemetic routines from: https://github.com/GaloisInc/cryptol-specs/blob/master/Primitive/Asymmetric/Signature/ECDSA/doc/10.1.1.204.9073.pdf
2020-09-22 19:58:15 +03:00
Cryptol.PrimeEC,
Add a Haskell-native implementation of the SHA256 and SHA512 block functions, ripped out of the SHA package, and expose it via new Cryptol primitives. Using these primitives in place of the defined reference implementations leads to approx 100x speed-up in larger protocols that do a lot of hashing. I don't know if this is the implementation we'll actually end up using, but this verifies the overall idea and helps design the API.
2020-09-04 19:03:58 +03:00
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Cryptol.Testing.Random,
split out notebook into separate package This involved: - Moving a couple REPL modules into the Cryptol library hierarchy (those that don't depend on console libraries) - Splitting up the Makefile, which unfortunately resulted in a lot of not-quite-duplication between the two Makefiles. Let's look into better abstraction...
2015-03-03 02:46:21 +03:00
Cryptol.Symbolic,
Break the symbolic query description datatypes into a separate module, moving SBV specific code into `Cryptol.Symbolic.SBV`
2020-03-24 02:57:31 +03:00
Cryptol.Symbolic.SBV,
Put together enough of the framework required to run `:sat` and `:prove` queries via What4. We still need to support configuring the solver to use, multisat queries, and portfolio solving.
2020-03-25 01:57:42 +03:00
Cryptol.Symbolic.What4,
Initial import from internal repo
2014-04-18 02:34:25 +04:00
split out notebook into separate package This involved: - Moving a couple REPL modules into the Cryptol library hierarchy (those that don't depend on console libraries) - Splitting up the Makefile, which unfortunately resulted in a lot of not-quite-duplication between the two Makefiles. Let's look into better abstraction...
2015-03-03 02:46:21 +03:00
Cryptol.REPL.Command,
Redo the scoping on the command line and browsing. This fixes a bug where the scoping on the command line was incorrect for nested modules. It also changes the semantics of `:browse` (whose implementation is now in a separate module), to be more reasonable. See #689
2021-04-03 02:07:48 +03:00
Cryptol.REPL.Browse,
split out notebook into separate package This involved: - Moving a couple REPL modules into the Cryptol library hierarchy (those that don't depend on console libraries) - Splitting up the Makefile, which unfortunately resulted in a lot of not-quite-duplication between the two Makefiles. Let's look into better abstraction...
2015-03-03 02:46:21 +03:00
Cryptol.REPL.Monad,
Cryptol.REPL.Trie
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Added SignCast instance and exported sbv Changes necessary for SAWCore's use of SBV. Ultimately, these should be merged into the upstream SBV package.
2014-08-06 20:49:19 +04:00
Other-modules: Cryptol.Parser.LexerUtils,
Cryptol.Parser.ParserUtils,
add "self-contained" mode for Cryptol-as-a-Library Many of our projects that depend on Cryptol break because we forgot to drag along `Cryptol.cry` or it just can't work out where it is from the perspective of the other executable. There's now a new flag `self-contained` in `cryptol.cabal` that is on by default that bakes the contents of the Prelude into the library, so that it can be reproduced on demand. This is really a hack at this point because the module system bakes in the assumption that a module has an associated file path, so we actually have to write the contents to a tmp file before reading them back in. Let's do better than this in the future. This option is disabled for targets in the Makefile because we want the standalone interpreter to be using the distribution's `Cryptol.cry`.
2015-03-06 02:14:09 +03:00
Cryptol.Prelude,
fixup: Paths_cryptol_parser
2014-04-18 21:28:46 +04:00
Paths_cryptol,
Initial import from internal repo
2014-04-18 02:34:25 +04:00
GitRev
Add INLINE and SPECIALIZE pragmas to generate better code for the concrete evaluator.
2020-03-30 23:01:06 +03:00
GHC-options: -Wall -fsimpl-tick-factor=140 -O2
clean up build a bit
2016-06-28 00:56:55 +03:00
if impl(ghc >= 8.0.1)
ghc-options: -Wno-redundant-constraints
Initial import from internal repo
2014-04-18 02:34:25 +04:00
distribution tweaks Makefile now has two modes depending on whether PREFIX is set. If it's not, we try to make the distribution as relocatable as possible, meaning we don't rely on the baked-in-by-cabal data directory. If it is set, we do use that path.
2015-03-04 03:22:14 +03:00
if flag(relocatable)
cpp-options: -DRELOCATABLE
Initial import from internal repo
2014-04-18 02:34:25 +04:00
executable cryptol
Add default-language to cabal file. Closes #71
2014-09-15 01:37:37 +04:00
Default-language:
Bump language standard to 2010. We're beyond '98 anyway...
2017-10-24 21:59:34 +03:00
Haskell2010
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Main-is: Main.hs
hs-source-dirs: cryptol
Fix some cabal warnings and such
2020-11-10 20:36:05 +03:00
Autogen-modules: Paths_cryptol
Initial import from internal repo
2014-04-18 02:34:25 +04:00
Other-modules: OptParser,
REPL.Haskeline,
another sdist fix
2015-01-28 22:28:52 +03:00
REPL.Logo,
fixup: Paths_cryptol_parser
2014-04-18 21:28:46 +04:00
Paths_cryptol
Fix some cabal warnings and such
2020-11-10 20:36:05 +03:00
add just enough strictness to evalCmd
2015-02-06 04:05:11 +03:00
build-depends: ansi-terminal
, base
use base-compat to remove much CPP
2015-10-09 02:54:08 +03:00
, base-compat
Improve tab completion for :set command. Fixes #154. Tab now completes option names after `:help :set`. Tab also completes `:help` with names of primitive types and type classes (cf. #504).
2018-07-31 04:11:08 +03:00
, containers
add just enough strictness to evalCmd
2015-02-06 04:05:11 +03:00
, cryptol
, directory
, filepath
Updates for haskeline 0.8 and use of exceptions package.
2020-05-07 00:14:47 +03:00
, haskeline >= 0.7 && < 0.9
start improving handling of interrupts in server This notably adds a `MonadBaseControl` instance for the `REPL` monad so that we can catch asynchronous exceptions in the middle of `REPL` computations. Since this is a generalization of Haskeline's exception support, that orphan instance for the console executable is now in terms of this new instance.
2015-12-04 02:36:43 +03:00
, monad-control
Implement module-name completion and validation for :browse. Fixes #396.
2017-10-05 05:15:42 +03:00
, text
add just enough strictness to evalCmd
2015-02-06 04:05:11 +03:00
, transformers
Add INLINE and SPECIALIZE pragmas to generate better code for the concrete evaluator.
2020-03-30 23:01:06 +03:00
GHC-options: -Wall -threaded -rtsopts "-with-rtsopts=-N1 -A64m" -O2
clean up build a bit
2016-06-28 00:56:55 +03:00
if impl(ghc >= 8.0.1)
ghc-options: -Wno-redundant-constraints
Initial import from internal repo
2014-04-18 02:34:25 +04:00
if os(linux) && flag(static)
Prep CI for upcoming release (#1123) - Container images are now published to ghcr.io rather than docker hub (closes #1110): - https://github.com/orgs/GaloisInc/packages/container/package/cryptol - https://github.com/orgs/GaloisInc/packages/container/package/cryptol-remote-api - Docker builds for all images are cached against ghcr.io (doesn't provide incremental builds, but it still helps a lot). - https://github.com/orgs/GaloisInc/packages/container/package/cache-cryptol - https://github.com/orgs/GaloisInc/packages/container/package/cache-cryptol-remote-api - "Portable" variant of cryptol-remote-api is now built and tested to the same degree as the non-portable one - Normalized CI workflows to [`.github/workflows/ci.yml`](https://github.com/GaloisInc/cryptol/blob/lisanna/docker-publishing/.github/workflows/ci.yml) (closes #1115) - Pre-merge and release build configurations are now more or less the same, so release process remains validated (closes #1114, closes #1116) - Matrix configs for each job are visible at high-level views of the workflow - Always upload workflow artifacts, use sensible retention periods for publish vs. non-publish - `cryptol-eval-server` included in cryptol-remote-api container image (closes #1112) - Pathclearing for static linking (#1113)
2021-03-24 01:24:48 +03:00
ld-options: -static -pthread
ghc-options: -optl-fuse-ld=bfd
fold server into main Cryptol package once merged, we'll disable the build by default so we don't incur the zeromq dependency, but it would be nice to eventually make the server the core of all our clients
2015-07-08 04:13:34 +03:00
Fix up html syntax highlighting.
2017-10-25 21:12:37 +03:00
executable cryptol-html
Update Cabal file for Hackage acceptance
2018-08-01 18:59:54 +03:00
Default-language:
Haskell2010
Fix up html syntax highlighting.
2017-10-25 21:12:37 +03:00
main-is: CryHtml.hs
hs-source-dirs: utils
Use blaze for HTML generation
2018-03-06 04:07:19 +03:00
build-depends: base, text, cryptol, blaze-html
Fix up html syntax highlighting.
2017-10-25 21:12:37 +03:00
GHC-options: -Wall
Prep CI for upcoming release (#1123) - Container images are now published to ghcr.io rather than docker hub (closes #1110): - https://github.com/orgs/GaloisInc/packages/container/package/cryptol - https://github.com/orgs/GaloisInc/packages/container/package/cryptol-remote-api - Docker builds for all images are cached against ghcr.io (doesn't provide incremental builds, but it still helps a lot). - https://github.com/orgs/GaloisInc/packages/container/package/cache-cryptol - https://github.com/orgs/GaloisInc/packages/container/package/cache-cryptol-remote-api - "Portable" variant of cryptol-remote-api is now built and tested to the same degree as the non-portable one - Normalized CI workflows to [`.github/workflows/ci.yml`](https://github.com/GaloisInc/cryptol/blob/lisanna/docker-publishing/.github/workflows/ci.yml) (closes #1115) - Pre-merge and release build configurations are now more or less the same, so release process remains validated (closes #1114, closes #1116) - Matrix configs for each job are visible at high-level views of the workflow - Always upload workflow artifacts, use sensible retention periods for publish vs. non-publish - `cryptol-eval-server` included in cryptol-remote-api container image (closes #1112) - Pathclearing for static linking (#1113)
2021-03-24 01:24:48 +03:00
if os(linux) && flag(static)
ld-options: -static -pthread
ghc-options: -optl-fuse-ld=bfd
Feature/docs checking (#976) * Adds a stub executable to cabal file for checking docs * [WIP] Adds check-exercises executable A program that checks that the exercises in Programming Cryptol actual work when executed against an Cryptol REPL. Instead of using \begin{Verbatim}, we use \begin{REPL} in both the exercise and the answer, which is rendered the same but gets checked by this program. This is a WIP -- we still need to do a number of things, including (but not limited to): * Move the "REPL" macro out of CrashCourse.tex and into some including latex file * Change many of the "Verbatim"s into "REPL"s to test if this approach works in general * Several updates * Moves REPL command definitions into main latex file * Generalizes repl commands * Several improvements: * documentation of CheckExercises.hs * factoring out addReplData, addReplin, addReplout, nextLine functions * took the IO out of P monad (shouldn't have been there) * worked on annotating repls for many exercises/examples in crash course * Adds a README for check-exercises * Uses cryptol's -e option to detect errors * updates ProgrammingCryptol.pdf * Fixes main function After changing to use the -e option to detect errors, I used cabal v2-exec which apparently does not rebuild anything, but I thought it did. This just fixes the code so it builds again.
2020-11-21 03:53:36 +03:00
executable check-exercises
Default-language:
Haskell2010
Main-is: CheckExercises.hs
hs-source-dirs: cryptol
build-depends: ansi-terminal
, base
, containers
, directory
, extra
, filepath
, mtl
, optparse-applicative
, process
, temporary
, text
GHC-options: -Wall
start benchmarking suite with a Prelude parse test
2015-08-10 21:24:36 +03:00
benchmark cryptol-bench
type: exitcode-stdio-1.0
main-is: Main.hs
hs-source-dirs: bench
default-language: Haskell2010
Add INLINE and SPECIALIZE pragmas to generate better code for the concrete evaluator.
2020-03-30 23:01:06 +03:00
GHC-options: -Wall -threaded -rtsopts "-with-rtsopts=-N1 -A64m" -O2
clean up build a bit
2016-06-28 00:56:55 +03:00
if impl(ghc >= 8.0.1)
ghc-options: -Wno-redundant-constraints
start benchmarking suite with a Prelude parse test
2015-08-10 21:24:36 +03:00
if os(linux) && flag(static)
Prep CI for upcoming release (#1123) - Container images are now published to ghcr.io rather than docker hub (closes #1110): - https://github.com/orgs/GaloisInc/packages/container/package/cryptol - https://github.com/orgs/GaloisInc/packages/container/package/cryptol-remote-api - Docker builds for all images are cached against ghcr.io (doesn't provide incremental builds, but it still helps a lot). - https://github.com/orgs/GaloisInc/packages/container/package/cache-cryptol - https://github.com/orgs/GaloisInc/packages/container/package/cache-cryptol-remote-api - "Portable" variant of cryptol-remote-api is now built and tested to the same degree as the non-portable one - Normalized CI workflows to [`.github/workflows/ci.yml`](https://github.com/GaloisInc/cryptol/blob/lisanna/docker-publishing/.github/workflows/ci.yml) (closes #1115) - Pre-merge and release build configurations are now more or less the same, so release process remains validated (closes #1114, closes #1116) - Matrix configs for each job are visible at high-level views of the workflow - Always upload workflow artifacts, use sensible retention periods for publish vs. non-publish - `cryptol-eval-server` included in cryptol-remote-api container image (closes #1112) - Pathclearing for static linking (#1113)
2021-03-24 01:24:48 +03:00
ld-options: -static -pthread
ghc-options: -optl-fuse-ld=bfd
start benchmarking suite with a Prelude parse test
2015-08-10 21:24:36 +03:00
build-depends: base
, criterion
, cryptol
add typechecking and large sequence benchmarks
2015-08-10 23:52:01 +03:00
, deepseq
Update benchmarks to find Prelude and CryptolTC.z3 Since they don’t run in the normal REPL environment, they need to know about where to find the Prelude and CryptolTC.z3 more directly.
2017-03-21 22:31:04 +03:00
, directory
, filepath
Set SBV bounds to >= 8.6 This is consistent with our current testing, and fixes #795
2020-06-30 20:15:32 +03:00
, sbv
start benchmarking suite with a Prelude parse test
2015-08-10 21:24:36 +03:00
, text
Reference in New Issue Copy Permalink