ConCert/dune-project at master · AU-COBRA/ConCert · GitHub

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
(lang dune 3.21)
(using rocq 0.11)
(name rocq-concert)
(version dev)

(generate_opam_files false)

(source (github AU-COBRA/ConCert))
(license MIT)
(authors "The COBRA team")
(maintainers "danil.v.annenkov@gmail.com")

(package
 (name rocq-concert)
 (synopsis "A framework for smart contract verification in Rocq")
 (depends
   (rocq-core (>= 9.1~))
   (rocq-stdlib (>= 9.0~))
   (rocq-bignums (>= 9~))
   (coq-quickchick (>= 2.0.4))
   (rocq-metarocq-utils (>= 1.4~))
   (rocq-metarocq-common (>= 1.4~))
   (rocq-metarocq-template (>= 1.4~))
   (rocq-metarocq-template-pcuic (>= 1.4~))
   (rocq-metarocq-pcuic (>= 1.4~))
   (rocq-metarocq-safechecker (>= 1.4~))
   (rocq-metarocq-erasure (>= 1.4~))
   (rocq-rust-extraction (= 0.2.0))
   (rocq-elm-extraction (= 0.2.0))
   (coq-stdpp (= 1.12.0))
   )
)

(package
 (name rocq-concert-examples)
 (synopsis "A framework for smart contract verification in Rocq")
 (depends
   (rocq-core (>= 9.1~))
   (rocq-stdlib (>= 9.0~))
   (rocq-bignums (>= 9~))
   (coq-quickchick (>= 2.0.4))
   (rocq-metarocq-utils (>= 1.4~))
   (rocq-metarocq-common (>= 1.4~))
   (rocq-metarocq-template (>= 1.4~))
   (rocq-metarocq-template-pcuic (>= 1.4~))
   (rocq-metarocq-pcuic (>= 1.4~))
   (rocq-metarocq-safechecker (>= 1.4~))
   (rocq-metarocq-erasure (>= 1.4~))
   (rocq-rust-extraction (= 0.2.0))
   (rocq-elm-extraction (= 0.2.0))
   (coq-stdpp (= 1.12.0))
   )
  (allow_empty)
)

(warnings (deprecated_coq_lang disabled))