The reference Qreals.Q2R was not found in the current environment

[jasonlarkin]

Hi,

I am trying to make all/examples/etc on the current, but getting the following error:

coqc -R . Top VOQC/RzQGateSet.v
File "./VOQC/RzQGateSet.v", line 29, characters 32-42:
Error: The reference Qreals.Q2R was not found in the current environment.

make: *** [Makefile:126: VOQC/RzQGateSet.vo] Error 1
(base) [jmlarkin@bridges2-login012 SQIR_fresh]$ git status
On branch main
Your branch is up to date with 'origin/main'.

commit 279121865607a069d96859c10edbbfcfe24b0dc7 (HEAD -> main, origin/main, origin/HEAD)
Merge: eb378d0 f72721d
Author: Kesha Hietala <kesha.hietala@gmail.com>
Date:   Thu Apr 29 18:50:56 2021 -0400

    Merge pull request #17 from inQWIRE/VOQC-journal

    Merging in the VOQC-journal branch

(base) [jmlarkin@bridges2-login012 SQIR_fresh]$ ../opam --version
2.0.8

(base) [jmlarkin@bridges2-login012 SQIR_fresh]$ coqc --version
The Coq Proof Assistant, version 8.13.2 (April 2021)
compiled on Apr 26 2021 1:01:13 with OCaml 4.12.0

[khieta]

Hi, as noted in our README we currently only support Coq version 8.12.0. See the notes under "Setup" for how to create an opam switch with Coq v8.12.0.

We hope to fix our proofs for v8.13.x at some point. In the meantime... sorry for the inconvenience. Feel free to submit a pull request if you want to fix things for us ;)

Let me know if switching to 8.12.0 fixes the problem!

[jasonlarkin]

Dangit! Sorry I missed that! I'm rebuilding everything now, thanks! Will update once compile is done (takes O(10) min).

@khieta new issue?

coqc --version
The Coq Proof Assistant, version 8.12.0 (May 2021)
compiled on May 4 2021 14:33:17 with OCaml 4.10.0

make clean
make all

coqc -R . Top SQIR/examples/QPEGeneral.v
File "./SQIR/examples/QPEGeneral.v", line 1, characters 29-35:
Error: Cannot find a physical path bound to logical path matching suffix
<> and prefix Interval.

make: *** [Makefile:79: SQIR/examples/QPEGeneral.vo] Error 1

And on a pull request to update to Coq v8.13.x, do you have any more notes/refs on what is necessary to get things updated (eg I assume it's more than Qreals.Q2R)?

[khieta]

@jasonlarkin Sorry for the delayed response! I've been traveling the past week. The issue in your last comment is most likely due to the Interval package not being installed (opam install coq-interval). Let me know if that fixes the problem.

My last commit (e60d8ca) should fix the issue with Coq v8.13.x.

[jasonlarkin]

You're right! Sorry I got mixed up with the different branches, all good now!

Btw this is an excellent tool and work, gracias!