Confusing warning: Using Vector.t is known to be technically difficult

[cogumbreiro]

Description of the problem

I was greeted with this warning:

Using Vector.t is known to be technically difficult, see <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v>.
[warn-library-file-stdlib-vector,stdlib-vector,warn-library-file,user-warn,default]

The message is ominous and unhelpful, as there is no course of action being proposed and the problem of difficulty is subjective. Furthermore, the URL is missing (404).

• Is the Vector library being deprecated?

I also am greeted with this warning:

Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.

I am not sure what is the intent behind the suggestion to use list bool.

I would be happy to submit a pull request on improving the warning message, and getting some clarity on the issue.

Thanks!

Small Rocq / Coq file to reproduce the bug

No response

Version of Rocq / Coq where this bug occurs

8.20

Last version of Rocq / Coq where the bug did not occur

No response

[andres-erbsen]

cc @proux01

[proux01]

The URL was indeed accidentaly broken, here is a fix: coq/coq#19911

About the message, I fully agree it's not ideal. It's unfortunately the trade off resulting of a very lengthy and painful discussion: coq/coq#18032
In particular, you can see in the discussion that we couldn't find 100% agreement to deprecate vectors, although the vast majority of Coq developpers agree that it just shouldn't be used (escept in very specific use cases like wanting to experience the difficulties arising with dependent pattern matching). For these reasons, I have personally absolutely no will to reopen that pandora box.

That being said, feel free to open a pull request to try to improve the message, but don't be surprised if faced with a lot of bikeshedding.

[cogumbreiro]

we couldn't find 100% agreement to deprecate vectors

I understand. So Bvectors are deprecated and that is noted in the warning messages and Vectors are not actually deprecated but their use is discouraged? I don't think the message makes that fact obvious.

Thank you for quickly fixing the URL, @proux01 .

Since I'm not really motivated to go through a bikeshedding session, I'll sit this one out. For my use case, it was quicker to reimplement Vector using sigma types and not depend on a potentially deprecated data type or deal with warning messages.

Thank you!

[Zimmi48]

Repeating my suggestion from coq/coq#19911 (comment). Someone should probably write a Platform Docs tutorial explaining why Vectors are generally not considered as a good idea, and we should link to this instead of a file in the repository.

[SkySkimmer]

"tutorial" doesn't sound like the right category for that