Define macros with CompCert's version number

[xavierleroy]

As suggested in #282, it can be useful to #ifdef code depending on specific versions of CompCert.

Assuming a version number of the form MM.mm or MM.mm.pp, the following macros are predefined:

__COMPCERT_MAJOR__=MM (the major version number)
__COMPCERT_MINOR__=mm (the minor version number)
__COMPCERT_PATCHLEVEL__=pp (the patchlevel, or 0 if none)
__COMPCERT_VERSION__=MMmm (two decimal digits each, e.g. 305 for version 3.5)

Having 3 macros for MAJOR, MINOR and PATCHLEVEL is what GCC and Clang do. (Edit: but during the discussion we found PATCHLEVEL useless.)

Having the combined VERSION macro is convenient to write tests such as

#if __COMPCERT_VERSION__ >= 302
// use feature introduced in CompCert 3.2
#endif

[m-schmidt]

There is a slight collision with our version numbers which look like 18.10 or 18.10i (2 digits for year and month plus optional i for intermediate releases). With our version number scheme __COMPCERT_PATCHLEVEL__ will always be zero.

Therefore it would be nice to add an additional define, e.g. __COMPCERT_BUILDNR__, which maps to Version.buildnr. Our build number is currently in the 4 million range but the integer range should suffice in the foreseeable future.

[m-schmidt]

Thanks, the extension looks good.

[xavierleroy]

You're right about __COMPCERT_BUILDNR__, I added a definition if the build number exists.

Concerning the 18.10 version numbers, I was not aware of this problem. Do you think the presence of __COMPCERT_BUILDNR__ is enough to distinguish between the two series of version numbers?

Finally, I'm not sure the PATCHLEVEL part is useful. For the public version the only cases where we've used 3-level version numbers was to adapt to several versions of Coq, e.g. 3.0 was for Coq 8.5 and 3.0.1 was for Coq 8.6 but otherwise functionally identical, so there was no point in announcing this difference to the C code that is being compiled.

Getting rid of the patchlevel part also makes the __COMPCERT_VERSION__ macro easier to read, e.g. 305 instead of 30500.

Opinions welcome!

[m-schmidt]

I think the presence of __COMPCERT_BUILDNR__ is sufficient to distinguish the two version number schemes, should if it ever be necessary. We also don't see a great benefit for an explicit patch level. It's easier to simply increment the minor version.

[xavierleroy]

OK, we're very much in agreement. I removed the PATCHLEVEL and simplified VERSION accordingly. The code also gets simpler.

[xavierleroy]

I have a feeling that we are all happy about this PR, so let me merge ASAP.