Stream: Coq devs & plugin devs

Topic: Error message on wrong-compiled .vo files in 8.12


view this post on Zulip Karl Palmskog (Jul 16 2020 at 16:54):

So I've played around with v8.12 for a while now. One in my mind quite big difference is that, when I try load .vo files that were compiled with another version of Coq (say, 8.11.2) I get a message along the lines of: "File.vo is corrupted" and nothing else.

This is very different from 8.11.2 and all previous versions, which were very specific about what the problem was, and talked about (something like) "File.vo signature was v8.10, expected v8.11". Is this an intentional change? I can get the exact error messages if there is interest.

view this post on Zulip Pierre-Marie P├ędrot (Jul 16 2020 at 17:14):

The fix has just been merged (https://github.com/coq/coq/pull/12677)

view this post on Zulip Karl Palmskog (Jul 16 2020 at 17:28):

thanks, was hard to know what to look for.


Last updated: Oct 15 2021 at 19:03 UTC