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