Coq or RoCQ?

[marcbezem]

The instructions in INSTALL are all about Coq. I installed RoQC. Is it possible to use Coq-HoTT with rocqide? If so, how?

[jdchristensen]

I don't think the name change Coq -> Rocq should affect anything, and Coq-HoTT works with the latest version of Rocq, so I think it should "just work". That said, I've never tried either coqide or rocqide myself. How did you install Rocq and Coq-HoTT? What happened when you tried rocqide?

[jdchristensen]

To add a bit more, when you install Coq-HoTT using opam or Rocq Platform, it should automatically install the Rocq compatibility wrappers, so that the old coq* commands are available and nothing in the build needs to change. I'll make a note in the INSTALL.md file. (Eventually, we'll make Rocq 9.0 our minimum version, and then can re-write everything to use "Rocq" instead of "Coq".)