adjust VSTlib opam config; fix util/make_version to work on MacOS

lib/_CoqProject

@@ -1,5 +1,6 @@
 -Q proof VSTlib
 -Q test VSTlibtest
+proof/version.v
 proof/math_extern.v
 proof/spec_math.v
 proof/verif_math.v

lib/coq-vst-lib.opam

@@ -1,12 +1,12 @@
 opam-version: "2.0"
-version: "dev"
+version: "2.12"
 synopsis: "VSTlib: VST-verified C library for VST-verified clients"
 description: "These program modules, in the form of Verified Software Units,
 may be linked with client-module code  (at the .c/.o level) and proofs (at the .v level)."
 authors: [
   "Andrew W. Appel"
 ]
-maintainer: "Andrew W. Appel"
+maintainer: "Andrew W. Appel <[email protected]>"
 homepage: "http://"
 dev-repo: "git+https://github.com/PrincetonUniversity/VST"
 bug-reports: "https://github.com/PrincetonUniversity/VST/issues"

lib/proof/version.v

@@ -0,0 +1,2 @@
+Require Import ZArith Coq.Strings.String. Open Scope string.
+Definition release := "2.12".

util/make_version

@@ -2,6 +2,11 @@
 #usage:  util/make_version Bitsize Compcert-version
 F=veric/version.v
 set -e
+if [ -f `which gdate` ]; then
+    DATE=gdate
+else
+    DATE=date
+fi
 printf >$F 'Require Import ZArith Coq.Strings.String. Open Scope string.\n'
 printf >>$F 'Definition git_rev := "'
 if [ -e "$(command -v git)" ] && [ "$(git rev-parse --is-inside-work-tree 2>/dev/null)" = "true" ]; then
@@ -12,7 +17,7 @@ printf >>$F 'Definition release := "'
 tr -d '[:cntrl:]' <VERSION >>$F
 printf >>$F '".\n'
 printf >>$F 'Definition date := "'
-date --rfc-3339=date | tr -d '[:cntrl:]' >>$F
+$DATE --rfc-3339=date | tr -d '[:cntrl:]' >>$F
 printf >>$F '".\n'
 printf >>$F 'Definition bitsize : Z := %d.\n' $1
 printf >>$F 'Definition compcert_version := "%s".' $2