Add a Version file allowing to identify the stdlib version from Rocq#263
Add a Version file allowing to identify the stdlib version from Rocq#263mattam82 wants to merge 1 commit into
Conversation
There was a problem hiding this comment.
why special handling of version here?
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
please add a comment about it then
| @@ -0,0 +1,2 @@ | |||
| From Corelib Require Import PrimString. | |||
| Definition version : string := "9.2". No newline at end of file | |||
There was a problem hiding this comment.
I guess a non-primstring-using alternative would be version : nat * nat := (9, 2)
IDK if depending on primstring is ever a problem
There was a problem hiding this comment.
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 ?
There was a problem hiding this comment.
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.
|
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 |
3 participants
Part of a fix for #256, allowing to identify the released version of stdlib however it has been installed.