why are new magic numbers not recognizable? E.g.
File /path/to/file.vo has bad magic number 81100 (expected 1131376929).
The vo file format changed.
But I thought that this particular bug was fixed?
(I mean that coqtop does a best effort to recognize the old vo format.)
it was https://github.com/coq/coq/issues/12513
(ftr 1131376929 is the ASCII encoding of "Coq!")
I got this today from 8.12.1 in CI
It seems the ASCII encoding *in decimal rather than hex" I guess?
But this error message matches the fix; it doesn't say "corrupted".
'It's all a matter of printing. It's a 32-bit big endian integer.)
what would you like to see as an error message?
This error means you're using vo files for Coq 8.11 inside Coq 8.12
hm. I only know the “expected” part conveys no information to me.
I should probably just ignore it
if that message is intentional, fine, just a weird intention.
Dunno, it's supposed to be fixed from now on, instead of changing at every Coq version.
but the version number is still there, just elsewhere, right?
(it could also print
expected “Coq!”, or “compiled with 8.11 and loaded with 8.12”, but that might be overly usable for Coq)
Yep, the version number is the next data in the vo. If you happen to load a vo file from two different >= 8.12 Coq versions, you'll get a proper version error.
The problem is that properly handling the change 8.11 -> 8.12 would have been slightly tedious for no good (future) reason.
So just for this version jump you'll get slightly weird error messages.
(pre-8.12, there was no distinction between the magic number and the version number.)
Last updated: Sep 28 2023 at 11:01 UTC