Skip to content

Commit

Permalink
Fix build according to README.md
Browse files Browse the repository at this point in the history
  • Loading branch information
jnfoster committed Feb 3, 2024
1 parent fb10faf commit 9508676
Show file tree
Hide file tree
Showing 6 changed files with 110 additions and 5 deletions.
1 change: 0 additions & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,6 @@ test: build

clean:
dune clean
rm -f petr4.opam poulet4.opam poulet4_Ccomp.opam

web:
dune build _build/default/web/web.bc.js --profile release && cp _build/default/web/web.bc.js web/html_build/
Expand Down
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ Alternatively, follow theses steps:
```
If this doesn't work, install the dependencies manually.
```
opam install ANSITerminal alcotest bignum cstruct-sexp pp ppx_deriving ppx_deriving_yojson yojson js_of_ocaml js_of_ocaml-lwt js_of_ocaml-ppx
opam install ANSITerminal alcotest bignum cstruct-sexp pp ppx_deriving ppx_import ppx_deriving_yojson yojson js_of_ocaml js_of_ocaml-lwt js_of_ocaml-ppx
```
1. Build bundled dependencies.
Expand Down
4 changes: 2 additions & 2 deletions bin/dune
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,11 @@
(name main)
(package petr4)
(modules main)
(libraries ANSITerminal core core_unix core_unix.command_unix petr4 alcotest poulet4 poulet4_Ccomp str)
(libraries ANSITerminal core core_unix core_unix.command_unix petr4 alcotest poulet4 str)
(preprocess (pps ppx_jane ppx_let)))

(executable
(name test)
(modules test)
(libraries ANSITerminal core core_unix core_unix.command_unix petr4 alcotest poulet4 poulet4_Ccomp p4stf str)
(libraries ANSITerminal core core_unix core_unix.command_unix petr4 alcotest poulet4 p4stf str)
(preprocess (pps ppx_jane)))
1 change: 0 additions & 1 deletion coq/extraction/dune
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,6 @@
countable
fin_maps
gmap
pmap
stringmap
option1
AList
Expand Down
62 changes: 62 additions & 0 deletions petr4.opam
Original file line number Diff line number Diff line change
@@ -0,0 +1,62 @@
# This file is generated by dune, edit dune-project instead
opam-version: "2.0"
version: "0.1.2"
synopsis: "Petr4: Formal Semantics for the P4 Programming Language"
maintainer: ["jnfoster@cs.cornell.edu"]
authors: [
"Ryan Doenges"
"Mina Tahmasbi Arashloo"
"Santiago Bautista"
"Alexander Chang"
"Newton Ni"
"Samwise Parkinson"
"Rudy Peterson"
"Alaia Solko-Breslin"
"Amanda Xu"
"Nate Foster"
]
license: "Apache-2.0"
homepage: "https://github.com/verified-network-toolchain/petr4"
bug-reports: "https://github.com/verified-network-toolchain/petr4"
depends: [
"conf-gmp"
"conf-m4"
"poulet4"
"poulet4_Ccomp"
"alcotest"
"bignum"
"ocaml" {>= "4.09.1"}
"dune" {>= "2.8" & >= "1.2"}
"cstruct"
"cstruct-sexp"
"menhir"
"ANSITerminal"
"core" {>= "v0.15.0" & < "v0.16.0"}
"pp" {>= "1.1.2"}
"ppx_deriving_yojson"
"ppx_import" {>= "0.15.0"}
"ppx_jane" {>= "0.15.0"}
"ppx_js_style" {>= "0.15.0"}
"ppx_let"
"yojson" {>= "1.7.0"}
"js_of_ocaml"
"js_of_ocaml-lwt"
"js_of_ocaml-ppx"
"p4pp" {>= "0.1.11"}
"coq" {>= "8.15.0" & < "8.17.0" & build}
"odoc" {with-doc}
]
build: [
["dune" "subst"] {dev}
[
"dune"
"build"
"-p"
name
"-j"
jobs
"@install"
"@runtest" {with-test}
"@doc" {with-doc}
]
]
45 changes: 45 additions & 0 deletions poulet4.opam
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
# This file is generated by dune, edit dune-project instead
opam-version: "2.0"
version: "0.1.0"
synopsis: "Poulet4: Petr4 in Coq"
maintainer: ["jnfoster@cs.cornell.edu"]
authors: [
"Ryan Doenges"
"Rudy Peterson"
"Qinshi Wang"
"Molly Pan"
"Shengyi Wang"
"John Chen"
"Eric Hayden Campbell"
"Parisa Ataei"
"Andrew Appel"
"Nate Foster"
]
license: "Apache-2.0"
homepage: "https://github.com/verified-network-toolchain/petr4"
bug-reports: "https://github.com/verified-network-toolchain/petr4"
depends: [
"bignum"
"dune" {>= "2.8" & build}
"coq" {>= "8.15.0" & < "8.17.0" & build}
"coq-equations" {build}
"coq-record-update" {build}
"coq-compcert" {build}
"coq-vst-zlist" {build}
"coq-stdpp" {build}
"odoc" {with-doc}
]
build: [
["dune" "subst"] {dev}
[
"dune"
"build"
"-p"
name
"-j"
jobs
"@install"
"@runtest" {with-test}
"@doc" {with-doc}
]
]

0 comments on commit 9508676

Please sign in to comment.