Update several packages for Coq 8.19 and recent releases

[andrew-appel]

Update the following packages for Coq 8.19 and for recent releases of other packages on which they depend:

coq-vcfloat
coq-vst
coq-vst-32
coq-vst-lib
coq-vst-zlist

[palmskog]

@andrew-appel standard advice I give these days: since GitHub no longer guarantees stability of generated archives such as https://github.com/VeriNum/vcfloat/archive/refs/tags/v2.2.tar.gz, you may want to manually upload an archive to GitHub as is done for Coq: https://github.com/coq/coq/releases/tag/V8.19.1 ( coq-8.19.1.tar.gz). Essentially, you can just download a generated archive and upload it again to ensure GitHub doesn't change the checksum over time.

[palmskog]

@andrew-appel the package coq-vst-zlist.2.14 is missing from the PR, which prevents building coq-vst.2.14. Could you please add the definition of coq-vst-zlist.2.14?

[andrew-appel]

coq-vst.2.14 now (correctly) depends on coq-vst-zlist.2.13 which did not need any updating (except that its opam now permits coq 8.19). Now use a special asset for coq-vst-2.14 and for coq-vcfloat-2.2 as suggested.

[palmskog]

@andrew-appel there is the following build error in CI for coq-vst-lib.2.13 on Coq 8.19.1:

# p14 : positive
# The term "Vfloat" has type "float -> val" while it is expected to have type
#  "match nonstd t with
#   | Some t0 => nonstd_rep t0
#   | None => Binary.binary_float (Z.pos ?p@{f1:=53}) ?z@{f2:=1024}
#   end -> val".
# 
# make[1]: *** [CoqMakefile:848: proof/spec_math.vo] Error 1
# make[1]: *** [proof/spec_math.vo] Deleting file 'proof/spec_math.glob'
# make[1]: *** Waiting for unfinished jobs....
# make: *** [Makefile:17: invoke-coqmakefile] Error 2

This is for the following possibly-relevant dependencies:

 - install coq                    8.19.1        [required by coq-vst-lib]
  - install elpi                   1.18.2        [required by coq-mathcomp-ssreflect]
  - install coq-vst-zlist          2.13          [required by coq-vst]
  - install coq-menhirlib          20231231      [required by coq-compcert]
  - install coq-flocq              4.1.4         [required by coq-vst-lib]
  - install coq-bignums            9.0.0+coq8.19 [required by coq-vcfloat]
  - install coq-elpi               2.0.2         [required by coq-hierarchy-builder]
  - install coq-compcert           3.13.1        [required by coq-vst-lib]
  - install coq-hierarchy-builder  1.7.0         [required by coq-mathcomp-ssreflect]
  - install coq-vst                2.14          [required by coq-vst-lib]
  - install coq-mathcomp-ssreflect 2.2.0         [required by coq-interval]
  - install coq-coquelicot         3.4.1         [required by coq-interval]
  - install coq-interval           4.10.0        [required by coq-vcfloat]
  - install coq-vcfloat            2.2           [required by coq-vst-lib]
  - install coq-vst-lib            2.13

Any ideas?

[palmskog]

We have a bunch of OOM kills and timeouts in CI. So due to CI limitations, doesn't look like we can check everything here, I'm going to merge and hope for the best...

[JasonGross]

I think this may have broken vcfloat on Coq 8.17, which presumably now needs an upper bound on the vst version.

2024-07-27T15:04:52.4718195Z # File "./Prune.v", line 1175, characters 5-10:
2024-07-27T15:04:52.4718632Z # Error: Not an inductive definition.
2024-07-27T15:04:52.4719105Z # 
2024-07-27T15:04:52.4719693Z # make: *** [Makefile:20: Prune.vo] Error 1

https://github.com/JasonGross/neural-net-coq-interp/actions/runs/10123036634/job/27998594050?pr=62

[andrew-appel]

I think this may have broken vcfloat on Coq 8.17, which presumably now needs an upper bound on the vst version.

coq-vcfloat doesn't depend on coq-vst, so it probably doesn't need an upper bound on the vst version. Just looking at the source code of Prune.v in github (without seeing the proof state in Coq), I'd guess one possibility is that coq-vcfloat.2.1.1 needs an upper bound on the coq-interval version, maybe "< 4.11~". And perhaps all versions of coq-vcfloat are broken by coq-interval.4.11.