CompCert dev: refresh the Menhir development patch, and fix the 32-bit Flocq bound

[JasonGross]

This fixes two independent failures in coq-compcert.dev and coq-compcert-32.dev; both are now green in CI.

Refresh the Menhir patch

The original claim that commit 34bf2ef made the patch redundant was incorrect:

$ gh api repos/AbsInt/CompCert/commits/34bf2ef
No commit found for SHA: 34bf2ef

Upstream master still extracts only digits from the Menhir version:

menhir_ver=$(menhir --version 2>/dev/null | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p')

Both recipes depend on "menhir" {... | = "dev"}, while a git-pinned Menhir reports menhir, version unreleased. The empty extracted version makes ./configure fail:

Testing Menhir... NOT FOUND
Error: make sure Menhir version 20200624 or later is installed.
One or several required tools are missing or too old.  Aborting.

The patch remained necessary but no longer applied because its context referenced MENHIR_REQUIRED=20190626, now 20200624. GNU patch tolerated the drift:

Hunk #1 succeeded at 616 with fuzz 2 (offset 60 lines)

Opam's patcher has no fuzz and rejected it:

These patches didn't apply at .../build/coq-compcert.dev:
  - 0001-Allow-dev-version-of-Menhir.patch:
    OpamSystem.Internal_patch_error("... does not apply cleanly.")

The refreshed patch uses git diff -U1 and a unique context line independent of MENHIR_REQUIRED. MSoegtrop's original commit header is preserved. Both copies and their extra-files: checksums are updated; this also resolves their previous divergence.

Require Flocq >= 4.0.0 for 32-bit CompCert

After the Menhir fix, coq-compcert-32.dev failed because this constraint selected coq-flocq.3.4.3:

"coq-flocq" {>= "3.1.0" & < "4.0.0"} | "coq-flocq3" {= "dev"}

  - install coq-flocq                3.4.3    [required by coq-compcert-32]

#=== ERROR while compiling coq-compcert-32.dev ===
# - ?Hmax: Cannot infer this placeholder of type "prec < emax" in
#   environment:
#   prec, emax : Z
#   prec_gt_0_ : Prec_gt_0 prec
#   prec_lt_emax_ : Prec_lt_emax prec emax
# make[1]: *** [Makefile:340: lib/IEEE754_extra.vo] Error 1

CompCert dev is 3.17 and bundles Flocq 4.2.2 (flocq/Version.v). The corrected bound matches coq-compcert.dev:

"coq-flocq" {>= "4.0.0" | = "dev"}

The nonexistent "coq-flocq3" {= "dev"} alternative is removed. The released coq-compcert-32.3.13.1 already requires {>= "4.1.0" & < "5~"}.

Validation

opam lint passes on both recipes, apart from pre-existing warning 62 for INRIA Non-Commercial License Agreement. The refreshed patch applies through opam's patcher and passes git apply --check.

Before the refresh, coq-compcert.dev failed on compilers 4.09.0, 4.14.2, and 5.3.0 with Testing Menhir... NOT FOUND; coq-compcert-32.dev failed likewise on 4.09.0 and 4.14.2 and was incompatible with 5.3.0. With only the Menhir fix, coq-compcert.dev succeeded on all three, while coq-compcert-32.dev reached and failed on Flocq for 4.09.0 and 4.14.2. The Flocq bound fixes those remaining jobs. Rebased onto ca01bfb4f.

Wordsmithed by Codex.