Update SQIR for QuantumLib >= 1.5.0, VOQC for >= 1.1.0 (#59)

* 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. * Fix typo * Version number bump
inQWIRE · Jul 29, 2024 · 321dfe1 · 321dfe1
1 parent 18300ad
commit 321dfe1
Show file tree

Hide file tree

Showing 5 changed files with 11 additions and 8 deletions.
diff --git 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
@@ -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 QuantumLib > 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
@@ -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
@@ -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
@@ -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
@@ -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}

diff --git 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))))