Rocq 9.0+rc1 has just been tagged

Announcements
1

Dear all,

The Rocq 9.0+rc1 tag has just been pushed. As per the release process,
package managers can start preparing package updates and library authors
can safely start preparing compatible releases.

Thank you for your attention,
PMP

2

Hi,

Congratulations on the big step forward!

Quick comment: I noticed that “coqc” is renamed to “rocq” and “coq_makefile” renamed to “rocq makefile”. I have not yet found out what “coqdep” has been renamed to.

I could dig this information from deep into the manual, but I would have expected such major changes to the binary names to appear (1) on the front page of the release, and (2) in the “recent change” log. I did not found them there.

For software (e.g software foundations) that used to be compatible the past two releases of coq/rocq, do you have any suggestion on how to offer backward compatibility (e.g. by means of aliases)? or would you say it’s hopeless?

Thanks,
Arthur

3

There is a coq opam package for version 9.0 which provides compatibility executables coqc coqdep etc
(the executables are actually in its dependency coq-core to be precise)

4

As for the documentation, it will be part of the release. It is just that people are still iterating on it and the release candidate was tagged without it. See here for a tentative documentation: Recent changes — The Rocq Prover 9.1+alpha documentation