Skip to content

Commit ab1b6bb

Browse files
JasonGrossJasonGross
authored
Add opam files, mostly from https://github.com/rocq-prover/opam (#2180)
1 parent 7e54556 commit ab1b6bb

File tree

3 files changed

+135
-0
lines changed

3 files changed

+135
-0
lines changed

‎coq-fiat-crypto-with-bedrock.opam‎

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
opam-version: "2.0"
2+
version: "dev"
3+
authors: [
4+
"Andres Erbsen <[email protected]>"
5+
"Google Inc."
6+
"Jade Philipoom <[email protected]> <[email protected]>"
7+
"Massachusetts Institute of Technology"
8+
"Zoe Paraskevopoulou <[email protected]>"
9+
]
10+
maintainer: "Jason Gross <[email protected]>"
11+
homepage: "https://github.com/mit-plv/fiat-crypto"
12+
bug-reports: "https://github.com/mit-plv/fiat-crypto/issues"
13+
license: "MIT OR Apache-2.0 OR BSD-1-Clause"
14+
build: [
15+
[make "-j%{jobs}%" "EXTERNAL_REWRITER=1" "EXTERNAL_COQPRIME=1" "coq" "standalone-unified-ocaml"]
16+
]
17+
install: [
18+
[make "EXTERNAL_REWRITER=1" "EXTERNAL_COQPRIME=1" "BINDIR=%{bin}%" "install" "install-standalone-unified-ocaml"]
19+
["etc/test-run-fiat-crypto-silent.sh" "%{bin}%/fiat_crypto"] {with-test}
20+
["etc/test-run-fiat-crypto-silent.sh" "fiat_crypto"] {with-test}
21+
]
22+
depends: [
23+
"conf-findutils" {build}
24+
"ocaml" {build & >= "4.08~"}
25+
"ocamlfind" {build}
26+
"coq" {>= "8.18~"}
27+
"coq-coqprime"
28+
"coq-rewriter"
29+
]
30+
conflict-class: [
31+
"coq-fiat-crypto"
32+
"coq-coqutil"
33+
"coq-bedrock2"
34+
"coq-rupicola"
35+
]
36+
dev-repo: "git+https://github.com/mit-plv/fiat-crypto.git"
37+
synopsis: "Cryptographic Primitive Code Generation by Fiat"
38+
description: """
39+
Coq code and proofs for a command-line binary that can synthesize proven-correct
40+
big-integer modular field arithmetic operations for cryptography.
41+
Target languages include C, Rust, Zig, Go, and bedrock2.
42+
"""
43+
tags: ["logpath:Crypto"]
44+
url {
45+
src: "git+https://github.com/mit-plv/fiat-crypto.git#master"
46+
}

‎coq-fiat-crypto-without-bedrock.opam‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
opam-version: "2.0"
2+
version: "dev"
3+
authors: [
4+
"Andres Erbsen <[email protected]>"
5+
"Google Inc."
6+
"Jade Philipoom <[email protected]> <[email protected]>"
7+
"Massachusetts Institute of Technology"
8+
"Zoe Paraskevopoulou <[email protected]>"
9+
]
10+
maintainer: "Jason Gross <[email protected]>"
11+
homepage: "https://github.com/mit-plv/fiat-crypto"
12+
bug-reports: "https://github.com/mit-plv/fiat-crypto/issues"
13+
license: "MIT OR Apache-2.0 OR BSD-1-Clause"
14+
build: [
15+
[make "-j%{jobs}%" "EXTERNAL_DEPENDENCIES=1" "SKIP_BEDROCK2=1" "coq-without-bedrock2" "standalone-unified-ocaml"]
16+
]
17+
install: [
18+
[make "EXTERNAL_DEPENDENCIES=1" "SKIP_BEDROCK2=1" "BINDIR=%{bin}%" "install-without-bedrock2" "install-standalone-unified-ocaml"]
19+
["etc/test-run-fiat-crypto-silent-no-bedrock2.sh" "%{bin}%/fiat_crypto"] {with-test}
20+
["etc/test-run-fiat-crypto-silent-no-bedrock2.sh" "fiat_crypto"] {with-test}
21+
]
22+
depends: [
23+
"conf-findutils" {build}
24+
"ocaml" {build & >= "4.08~"}
25+
"ocamlfind" {build}
26+
"coq" {>= "8.18~"}
27+
"coq-coqprime"
28+
"coq-rewriter"
29+
"coq-coqutil"
30+
]
31+
conflict-class: [
32+
"coq-fiat-crypto"
33+
]
34+
dev-repo: "git+https://github.com/mit-plv/fiat-crypto.git"
35+
synopsis: "Cryptographic Primitive Code Generation by Fiat"
36+
description: """
37+
Coq code and proofs for a command-line binary that can synthesize proven-correct
38+
big-integer modular field arithmetic operations for cryptography.
39+
Target languages include C, Rust, Zig, and Go.
40+
"""
41+
tags: ["logpath:Crypto"]
42+
url {
43+
src: "git+https://github.com/mit-plv/fiat-crypto.git#master"
44+
}

‎coq-fiat-crypto.opam‎

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
opam-version: "2.0"
2+
version: "dev"
3+
authors: [
4+
"Andres Erbsen <[email protected]>"
5+
"Google Inc."
6+
"Jade Philipoom <[email protected]> <[email protected]>"
7+
"Massachusetts Institute of Technology"
8+
"Zoe Paraskevopoulou <[email protected]>"
9+
]
10+
maintainer: "Jason Gross <[email protected]>"
11+
homepage: "https://github.com/mit-plv/fiat-crypto"
12+
bug-reports: "https://github.com/mit-plv/fiat-crypto/issues"
13+
license: "MIT OR Apache-2.0 OR BSD-1-Clause"
14+
build: [
15+
[make "-j%{jobs}%" "EXTERNAL_DEPENDENCIES=1" "SKIP_COQSCRIPTS_INCLUDE=1" "coq" "standalone-ocaml"]
16+
]
17+
install: [
18+
[make "EXTERNAL_DEPENDENCIES=1" "SKIP_COQSCRIPTS_INCLUDE=1" "BINDIR=%{bin}%" "install" "install-standalone-unified-ocaml"]
19+
["etc/test-run-fiat-crypto-silent.sh" "%{bin}%/fiat_crypto"] {with-test}
20+
["etc/test-run-fiat-crypto-silent.sh" "fiat_crypto"] {with-test}
21+
]
22+
depends: [
23+
"conf-findutils" {build}
24+
"ocaml" {build & >= "4.08~"}
25+
"ocamlfind" {build}
26+
"coq" {>= "8.18~"}
27+
"coq-coqprime" {>= "1.2.0" | = "dev"}
28+
"coq-rewriter" {( >= "0.0.6" & <= "0.0.9" ) | = "dev"}
29+
"coq-rupicola" {= "0.0.8" | = "dev"}
30+
"coq-bedrock2-compiler" {= "0.0.6" | = "dev"}
31+
]
32+
conflict-class: [
33+
"coq-fiat-crypto"
34+
]
35+
dev-repo: "git+https://github.com/mit-plv/fiat-crypto.git"
36+
synopsis: "Cryptographic Primitive Code Generation by Fiat"
37+
description: """
38+
Coq code and proofs for a command-line binary that can synthesize proven-correct
39+
big-integer modular field arithmetic operations for cryptography.
40+
Target languages include C, Rust, Zig, Go, and bedrock2.
41+
"""
42+
tags: ["logpath:Crypto"]
43+
url {
44+
src: "git+https://github.com/mit-plv/fiat-crypto.git#master"
45+
}

0 commit comments

Comments
 (0)