This repository has been archived by the owner on May 6, 2021. It is now read-only.
forked from jonathan-laurent/copilot-kind
-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathcopilot-theorem.cabal
116 lines (99 loc) · 4.98 KB
/
copilot-theorem.cabal
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
cabal-version : >= 1.10
name : copilot-theorem
synopsis: k-induction for Copilot.
description:
Some tools to prove properties on Copilot programs with k-induction model
checking.
.
Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in
Haskell that compiles into embedded C. Copilot contains an interpreter,
multiple back-end compilers, and other verification tools.
.
A tutorial, examples, and other information are available at
<https://copilot-language.github.io>.
version : 3.2.1
license : BSD3
license-file : LICENSE
maintainer : [email protected]
homepage : https://copilot-language.github.io
bug-reports : https://github.com/Copilot-Language/copilot-theorem/issues
stability : Experimental
category : Language, Embedded
build-type : Simple
extra-source-files : README.md
, CHANGELOG
author : Jonathan Laurent
library
default-language : Haskell2010
hs-source-dirs : src
ghc-options : -Wall -fwarn-tabs
-fno-warn-name-shadowing
-fno-warn-unused-binds
-fno-warn-missing-signatures
-fcontext-stack=100
-- -fpackage-trust
-- -trust=array
-- -trust=base
-- -trust=containers
-- -- -trust=copilot-core
-- -trust=directory
-- -- -trust=exceptions
-- -trust=process
-- -- -trust=random
-- -trust=unix
-- -- -trust=parsec
-- -trust=bytestring
-- -- -trust=text
build-depends : base >= 4.9 && < 5
, ansi-terminal >= 0.8 && < 0.10
, bimap >= 0.3 && < 0.4
, bv-sized >= 1.0.2 && < 1.1
, containers >= 0.4 && < 0.7
, data-default >= 0.7 && < 0.8
, directory >= 1.3 && < 1.4
, filepath >= 1.4.2 && < 1.5
, mtl >= 2.0 && < 2.3
, panic >= 0.4.0 && < 0.5
, parsec >= 2.0 && < 3.2
, parameterized-utils >= 2.1.1 && < 2.2
, pretty >= 1.0 && < 1.2
, process >= 1.6 && < 1.7
, random >= 1.1 && < 1.2
, transformers >= 0.5 && < 0.6
, xml >= 1.3 && < 1.4
, what4 >= 1.0 && < 1.1
, copilot-core >= 3.2.1 && < 3.3
exposed-modules : Copilot.Theorem
, Copilot.Theorem.Prove
, Copilot.Theorem.Kind2
, Copilot.Theorem.Prover.SMT
-- , Copilot.Theorem.Prover.Z3
, Copilot.Theorem.Kind2.Prover
, Copilot.Theorem.What4
other-modules : Copilot.Theorem.Tactics
, Copilot.Theorem.IL
, Copilot.Theorem.IL.PrettyPrint
, Copilot.Theorem.IL.Spec
, Copilot.Theorem.IL.Translate
, Copilot.Theorem.IL.Transform
, Copilot.Theorem.Kind2.AST
, Copilot.Theorem.Kind2.Output
, Copilot.Theorem.Kind2.PrettyPrint
, Copilot.Theorem.Kind2.Translate
, Copilot.Theorem.Prover.SMTIO
, Copilot.Theorem.Prover.SMTLib
, Copilot.Theorem.Prover.TPTP
, Copilot.Theorem.Prover.Backend
, Copilot.Theorem.Misc.Error
, Copilot.Theorem.Misc.SExpr
, Copilot.Theorem.Misc.Utils
, Copilot.Theorem.TransSys
, Copilot.Theorem.TransSys.Cast
, Copilot.Theorem.TransSys.PrettyPrint
, Copilot.Theorem.TransSys.Renaming
, Copilot.Theorem.TransSys.Spec
, Copilot.Theorem.TransSys.Transform
, Copilot.Theorem.TransSys.Translate
, Copilot.Theorem.TransSys.Invariants
, Copilot.Theorem.TransSys.Operators
, Copilot.Theorem.TransSys.Type