Stream: Coq users

Topic: Coq 8.12 strange magic numbers


view this post on Zulip 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).

view this post on Zulip Pierre-Marie Pédrot (Nov 23 2020 at 22:31):

The vo file format changed.

view this post on Zulip Pierre-Marie Pédrot (Nov 23 2020 at 22:31):

But I thought that this particular bug was fixed?

view this post on Zulip Pierre-Marie Pédrot (Nov 23 2020 at 22:32):

(I mean that coqtop does a best effort to recognize the old vo format.)

view this post on Zulip Pierre-Marie Pédrot (Nov 23 2020 at 22:32):

it was https://github.com/coq/coq/issues/12513

view this post on Zulip Pierre-Marie Pédrot (Nov 23 2020 at 22:35):

(ftr 1131376929 is the ASCII encoding of "Coq!")

view this post on Zulip Paolo Giarrusso (Nov 23 2020 at 22:40):

I got this today from 8.12.1 in CI

view this post on Zulip Paolo Giarrusso (Nov 23 2020 at 22:40):

It seems the ASCII encoding *in decimal rather than hex" I guess?

view this post on Zulip Paolo Giarrusso (Nov 23 2020 at 22:43):

But this error message matches the fix; it doesn't say "corrupted".

view this post on Zulip 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.)

view this post on Zulip Paolo Giarrusso (Nov 23 2020 at 22:43):

Sure

view this post on Zulip Pierre-Marie Pédrot (Nov 23 2020 at 22:44):

what would you like to see as an error message?

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Nov 23 2020 at 22:45):

hm. I only know the “expected” part conveys no information to me.

view this post on Zulip Paolo Giarrusso (Nov 23 2020 at 22:45):

I should probably just ignore it

view this post on Zulip Paolo Giarrusso (Nov 23 2020 at 22:46):

if that message is intentional, fine, just a weird intention.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 23 2020 at 22:49):

but the version number is still there, just elsewhere, right?

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Nov 23 2020 at 22:52):

So just for this version jump you'll get slightly weird error messages.

view this post on Zulip 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: Feb 06 2023 at 13:03 UTC