-
Notifications
You must be signed in to change notification settings - Fork 5
/
Copy pathCargo.toml
95 lines (86 loc) · 2.87 KB
/
Cargo.toml
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
[workspace]
members = [
"scooter",
"jani",
"z3rro"
]
[package]
name = "caesar"
version = "2.1.2"
authors = ["Philipp Schroer <[email protected]>"]
description = "Caesar is a deductive verifier for probabilistic programs."
homepage = "https://www.caesarverifier.org/"
repository = "https://github.com/moves-rwth/caesar"
license = "MIT"
keywords = ["verification", "probabilistic programming"]
edition = "2021"
build = "build.rs" # LALRPOP preprocessing
[features]
default = ["static-link-z3"]
datatype-eureal = ["z3rro/datatype-eureal"]
datatype-eureal-funcs = ["z3rro/datatype-eureal-funcs"]
static-link-z3 = ["z3/static-link-z3"]
# Emit log messages to stderr without timing information. This is useful to diff logs.
log-print-timeless = []
[dependencies]
string-interner = "0.18"
lalrpop-util = { version = "0.22", features = ["lexer"] }
z3 = "^0.12"
z3-sys = "^0.8"
ref-cast = "1.0"
replace_with = "0.1"
num = "0.4"
tracing = "0.1"
tracing-subscriber = { version = "^0.3.3", features = ["env-filter", "json"] }
pathdiff = "0.2"
egg = "0.9"
tokio = { version = "1", features = ["time", "macros", "rt", "rt-multi-thread"] }
simple-process-stats = "1.0"
hdrhistogram = "7.5"
ariadne = "0.5"
thiserror = "2.0"
indexmap = "2.7"
pretty = "0.12"
z3rro = { path = "./z3rro" }
dashmap = "5.4"
im-rc = "15"
cfg-if = "1.0.0"
lsp-types = "0.97.0"
serde_json = "1.0.114"
lsp-server = "0.7.6"
serde = "1.0.197"
jani = { path = "./jani" }
itertools = "0.13.0"
stacker = "0.1.15"
crossbeam-channel = "0.5.14"
shlex = "1.3.0"
clap = { version = "4.5.23", features = ["derive", "string", "cargo"] }
clap_complete = "4.5.42"
regex = "1.11.1"
tempfile = "3.16.0"
[build-dependencies]
lalrpop = "0.22"
built = { version = "0.7", features = ["git2", "chrono"] }
[dev-dependencies]
glob = "0.3"
proptest = "1.6"
pretty_assertions = "1.4.0"
libtest-mimic = "0.8.1"
[[test]]
name = "integration"
path = "tests/integration.rs"
harness = false
# Unfortunately, adding debug information to release binaries incurs
# an unacceptable overhead of about 450 megabytes. So we disable it.
# debug = "line-tables-only"
# there are tests which take more than 10x longer with z3 not optimized, so just optimize z3 as well as possible.
# this might make some debugging a bit harder, so you might want to disable it for that.
[profile.dev.package.z3-sys]
opt-level = 3
[patch.crates-io]
z3 = { git = 'https://github.com/Philipp15b/z3.rs.git', rev = 'bdd501ca1e50785365b875b3438a0cf953cffbfc' }
z3-sys = { git = 'https://github.com/Philipp15b/z3.rs.git', rev = 'bdd501ca1e50785365b875b3438a0cf953cffbfc' }
# to work on z3.rs locally, clone it into the main directory and use the following directive instead:
# z3 = { path = 'z3.rs/z3' }
# see https://github.com/heim-rs/darwin-libproc/pull/3#issuecomment-1645444056
darwin-libproc = { git = "https://github.com/Orycterope/darwin-libproc.git", rev = "f73ddb1002d51ae74c1b41670fae56bd5896b7a3" }