clightgen should produce configuration information

[andrew-appel]

It would be very useful if clightgen, compiling foo.c into foo.v, would record information about the configuration, in particular,

(1) the following information from Makefile.config
ARCH, BITSIZE, ENDIANNESS

(2) version of CompCert
Version number (e.g., 3.2)
Git commit number

(3) the following information from command-line arguments
filename (e.g., foo.c)
-normalize (true or false)

(4) date/time that clightgen was run

This information should be in a Coq structure, not in a comment, so that tools that import foo.v can query it directly.

Why would this be useful? If the configuration of CompCert does not match the configuration of another tool such as VST, then the foo.v file will be subtly incompatible, causing difficult-to-diagnose bugs. This explicit configuration information will make the diagnosis easy.

[xavierleroy]

I see no one followed up on this suggestion; sorry about that. Globally it looks good. However:

(2) Git commit number

This is notoriously hard to include in a program, see e.g. https://stackoverflow.com/questions/3442874/in-git-how-can-i-write-the-current-commit-hash-to-a-file-in-the-same-commit

(4) date/time that clightgen was run

Timestamps have little value and prevent reproducible builds.

[xavierleroy]

See proposal at #238. Please review.

[andrew-appel]

Looks good. Thank you.

[xavierleroy]

Thanks for the review. It's merged.