From 9508676128a00ec5b23da4139c3c74849f2a8b1c Mon Sep 17 00:00:00 2001
From: Nate Foster <jnfoster@cs.cornell.edu>
Date: Sat, 3 Feb 2024 22:22:45 +0100
Subject: [PATCH] Fix build according to README.md

---
 Makefile            |  1 -
 README.md           |  2 +-
 bin/dune            |  4 +--
 coq/extraction/dune |  1 -
 petr4.opam          | 62 +++++++++++++++++++++++++++++++++++++++++++++
 poulet4.opam        | 45 ++++++++++++++++++++++++++++++++
 6 files changed, 110 insertions(+), 5 deletions(-)
 create mode 100644 petr4.opam
 create mode 100644 poulet4.opam

diff --git a/Makefile b/Makefile
index e46cf7cef..c10e5bbb5 100644
--- a/Makefile
+++ b/Makefile
@@ -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/
diff --git a/README.md b/README.md
index 2f656a37d..c35b2fec7 100644
--- a/README.md
+++ b/README.md
@@ -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.
diff --git a/bin/dune b/bin/dune
index 869f9925a..417f1e477 100644
--- a/bin/dune
+++ b/bin/dune
@@ -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)))
diff --git a/coq/extraction/dune b/coq/extraction/dune
index 197933a5e..e780546e5 100644
--- a/coq/extraction/dune
+++ b/coq/extraction/dune
@@ -9,7 +9,6 @@
   countable
   fin_maps
   gmap
-  pmap
   stringmap
   option1
   AList
diff --git a/petr4.opam b/petr4.opam
new file mode 100644
index 000000000..309c42948
--- /dev/null
+++ b/petr4.opam
@@ -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}
+  ]
+]
diff --git a/poulet4.opam b/poulet4.opam
new file mode 100644
index 000000000..89d8bffd0
--- /dev/null
+++ b/poulet4.opam
@@ -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}
+  ]
+]