Move Shor proofs to a separate repository

[khieta]

It would be cleaner to have the Shor proof (currently in examples/shor) in a separate repository. It is the largest application of SQIR, aside from VOQC, and it has different dependencies from the rest of SQIR (euler and coq-interval). We should also update the Shor proofs to use the modular multiplier defined in VQO instead of the old ModMult.v and RCIR.v files.

My proposal: make a new repository called SQIR-shor that contains the current content of examples/shor. This repository will need to link the SQIR, VQO, and euler repositories as submodules. It might take some effort to get the build working.

Open to opinions.

[rnrand]

VOQC is by far the largest SQIR application, and I'd personally say that it makes even more sense to have as its own repo. On the other hand, there are far larger repositories than SQIR (or even SQIR+VQO+QuantumLib or everything in INQWIRE), and I'm not convinced that the proliferation of small dependent libraries makes anyone's life easier. All things equal, I'd just leave things as they are.

(And installing packages like Interval seem like far less overhead than it once was.)

That said, if @PicksPeng wants to split off and maintain Shor as a separate library, I wouldn't object too much. I would recommend keeping it in INQWIRE and under an MIT license, though. (I can create the new repo if needed.)

[khieta]

Like I said, I'm open to other opinions.

The main issue is that if we update the Shor proofs to use the VQO oracles (which we should!) then we would need to move VQO back inside of SQIR, which I'd prefer not to do because it will make SQIR larger and harder to maintain. Aesthetically, I prefer more smaller repos over one large repo.

[rnrand]

I was just thinking, maybe make VQO and Shor top level in the SQIR repo?

Maintaining Shor will be tricky anyway, given its dependencies.

[PicksPeng]

I'm open to this idea. I don't think the additional organizing work is very worthwhile for the time consumption. I love the idea of using the VQO oracles, but I'm not very familiar with the VQO codebase so maybe @liyili2 can take a look at this part. I think the current codebase is well-organized compared to many other famous projects and is small enough to maintain.