From d814f09fb59611fd2e1901d494f98de9c7270154 Mon Sep 17 00:00:00 2001
From: William Spencer <wjbs@uchicago.edu>
Date: Mon, 15 Jul 2024 18:28:40 -0700
Subject: [PATCH 1/3] Fixed instance of Qsimpl hanging in SQIR with Qlib >= 1.4
 (issue resolved by patch to Qlib, but this fix is independent). Updated .opam
 files to reflect new compatibility with Qlib >= 1.4, though only >= 1.5 for
 SQIR as an import issue in Qlib has to be resolved in a way breaking
 backwards-compatibility.

---
 SQIR/UnitaryOps.v                   | 2 +-
 VOQC/RemoveZRotationBeforeMeasure.v | 3 +++
 coq-sqir.opam                       | 2 +-
 coq-voqc.opam                       | 2 +-
 4 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/SQIR/UnitaryOps.v b/SQIR/UnitaryOps.v
index 5f5e84b..f6f1d69 100644
--- a/SQIR/UnitaryOps.v
+++ b/SQIR/UnitaryOps.v
@@ -1,5 +1,5 @@
 Require Export UnitarySem.
-Require Export QuantumLib.VectorStates.
+Require Export QuantumLib.VectorStates QuantumLib.Bits.
 
 (* This file contains useful operations over unitary programs including:
    - inversion
diff --git a/VOQC/RemoveZRotationBeforeMeasure.v b/VOQC/RemoveZRotationBeforeMeasure.v
index b6c2805..c6a7890 100644
--- a/VOQC/RemoveZRotationBeforeMeasure.v
+++ b/VOQC/RemoveZRotationBeforeMeasure.v
@@ -81,6 +81,9 @@ Proof.
   repeat rewrite Mmult_assoc.
   Msimpl.
   repeat (restore_dims; rewrite <- Mmult_assoc).
+  (* This line is extraneous with the patch to 
+     Qsimpl / Q_db in QuantumLim > 1.5.0 *)
+  replace (σx †) with σx by (symmetry; apply σx_hermitian).
   Qsimpl.
   rewrite Mplus_comm; reflexivity.
   rewrite Mplus_comm; reflexivity.
diff --git a/coq-sqir.opam b/coq-sqir.opam
index 617d0f8..a4f43e7 100644
--- a/coq-sqir.opam
+++ b/coq-sqir.opam
@@ -14,7 +14,7 @@ bug-reports: "https://github.com/inQWIRE/SQIR/issues"
 depends: [
   "dune" {>= "3.8"}
   "coq-interval" {>= "4.9.0"}
-  "coq-quantumlib" {= "1.3.0"}
+  "coq-quantumlib" {>= "1.5.0"}
   "coq" {>= "8.16"}
   "odoc" {with-doc}
 ]
diff --git a/coq-voqc.opam b/coq-voqc.opam
index c9eca2d..308caad 100644
--- a/coq-voqc.opam
+++ b/coq-voqc.opam
@@ -14,7 +14,7 @@ bug-reports: "https://github.com/inQWIRE/SQIR/issues"
 depends: [
   "dune" {>= "2.8"}
   "coq-interval" {>= "4.6.1"}
-  "coq-quantumlib" {>= "1.1.0" < "1.4.0"}
+  "coq-quantumlib" {>= "1.1.0"}
   "coq-sqir" {>= "1.3.0"}
   "coq" {>= "8.12"}
   "odoc" {with-doc}

From 172f870bae3ccbf8f3b08f0b825e018348d6410a Mon Sep 17 00:00:00 2001
From: William Spencer <wjbs@uchicago.edu>
Date: Mon, 15 Jul 2024 18:42:43 -0700
Subject: [PATCH 2/3] Fix typo

---
 VOQC/RemoveZRotationBeforeMeasure.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/VOQC/RemoveZRotationBeforeMeasure.v b/VOQC/RemoveZRotationBeforeMeasure.v
index c6a7890..d494028 100644
--- a/VOQC/RemoveZRotationBeforeMeasure.v
+++ b/VOQC/RemoveZRotationBeforeMeasure.v
@@ -82,7 +82,7 @@ Proof.
   Msimpl.
   repeat (restore_dims; rewrite <- Mmult_assoc).
   (* This line is extraneous with the patch to 
-     Qsimpl / Q_db in QuantumLim > 1.5.0 *)
+     Qsimpl / Q_db in QuantumLib > 1.5.0 *)
   replace (σx †) with σx by (symmetry; apply σx_hermitian).
   Qsimpl.
   rewrite Mplus_comm; reflexivity.

From 244b136df08906055012dec78cb8a85f24659e5d Mon Sep 17 00:00:00 2001
From: William Spencer <wjbs@uchicago.edu>
Date: Mon, 29 Jul 2024 12:45:25 -0700
Subject: [PATCH 3/3] Version number bump

---
 coq-sqir.opam | 2 +-
 coq-voqc.opam | 2 +-
 dune-project  | 6 +++---
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/coq-sqir.opam b/coq-sqir.opam
index a4f43e7..3efcd97 100644
--- a/coq-sqir.opam
+++ b/coq-sqir.opam
@@ -1,6 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "1.3.0"
+version: "1.3.1"
 synopsis: "Coq library for reasoning about quantum circuits"
 description: """
 inQWIRE's SQIR is a Coq library for reasoning
diff --git a/coq-voqc.opam b/coq-voqc.opam
index 308caad..b53d2f0 100644
--- a/coq-voqc.opam
+++ b/coq-voqc.opam
@@ -1,6 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "1.3.0"
+version: "1.3.1"
 synopsis: "A verified optimizer for quantum compilation"
 description: """
 inQWIRE's VOQC is a Coq library for verified
diff --git a/dune-project b/dune-project
index 81e4a85..40c50a4 100644
--- a/dune-project
+++ b/dune-project
@@ -1,6 +1,6 @@
 (lang dune 3.8)
 (name coq-sqirvoqc)
-(version 1.3.0)
+(version 1.3.1)
 (using coq 0.7)
 (generate_opam_files true)
 
@@ -17,7 +17,7 @@
  )
  (depends
    (coq-interval (>= 4.9.0))
-   (coq-quantumlib (= 1.3.0))
+   (coq-quantumlib (>= 1.5.0))
    (coq (>= 8.16))))
 
 (package
@@ -28,6 +28,6 @@
  )
  (depends
    (coq-interval (>= 4.9.0))
-   (coq-quantumlib (>= 1.3.0))
+   (coq-quantumlib (>= 1.5.0))
    (coq-sqir (>= 1.3.0))
    (coq (>= 8.16))))