Add a Version file allowing to identify the stdlib version from Rocq

[mattam82]

Part of a fix for #256, allowing to identify the released version of stdlib however it has been installed.

• Added changelog. (is this necessary?)
• Added / updated documentation. (notes for the release process)

[SkySkimmer]

why special handling of version here?

[mattam82]

This avoids an issue with the sed below which replaces ./ with From .... In the output of the rocq dep call, we get Version.v not ./Version.v.

[SkySkimmer]

please add a comment about it then

[SkySkimmer]

I guess a non-primstring-using alternative would be version : nat * nat := (9, 2)

IDK if depending on primstring is ever a problem

[mattam82]

I don't know what's the best representation here either, I thought a simple string representation would be simpler to interpret by clients. I refrained from using String as it would add a dependency, on the other hand Flocq is parsing a string and encoding it using N (https://gitlab.inria.fr/flocq/flocq/-/blob/master/src/Version.v.in?ref_type=heads) What's the benefit of that representation @silene ?

[silene]

I wanted something I could easily perform comparisons on, in Gallina (or by extension, Ltac). Using numbers makes things easy; strings not so much. (It is the usual issue, "x.10" is not lexicographically larger than "x.9".) But in the end, I do not think I ever used that feature.

[SkySkimmer]

We could also use ltac2 (Ltac2 rocq_version () := "9.2") since it has strings without depending on primstring (primitives get reported as axioms by Print Assumptions so depending on it could be annoying).
Then if someone wants to turn it into a term they can do whatever they like.

[SkySkimmer]

btw if we can finish rocq-prover/rocq#21564, it seems ocamlfind files have a version field

[mattam82]

btw if we can finish rocq-prover/rocq#21564, it seems ocamlfind files have a version field

Yes, it would be another way to go

[andres-erbsen]

How is this related to #256? What's the plan? (I thought we agreed to keep the versions in sync, so I don't understand why rocq will need to look at a version file in stdlib.)

[xavierleroy]

I thought we agreed to keep the versions in sync

I'm afraid they haven't agreed. Sadly.

[xavierleroy]

I don't know what's the best representation here either, I thought a simple string representation would be simpler to interpret by clients.

I tend to agree. If the version check is to be performed by a configure script (as in CompCert), something like the following should work:

echo "Require Version. Print Version.version." > PrintVersion.v
stdlib_version=$(rocq top -batch -load-vernac-source PrintVersion.v | sed -n -e 's/Version.version = "\(.*\)".*$/\1/p')

Not great, but workable.

[andres-erbsen]

I am referring to the discussion last Tuesday -- there's no disagreement in the notes, and I don't remember hearing any. Thus I am extra surprised to see a version-checking hook proposed now.

[proux01]

@mattam82 since rocq-prover/rocq#21564 got in, do we still need this?

[SkySkimmer]

Although it's possible to put some version info in the META I don't think we actually do it so that PR probably isn't useful for this problem?