Stream: math-comp users

Topic: Mixing MC 2.0 and MC 1.17

view this post on Zulip Pierre Jouvelot (Dec 06 2023 at 09:02):

I would like to mix some Coq developments between these two versions of MC. I have a small file I developed using MC 2.0 that I would like to reuse in an older code base that uses MC 1.17. Can I just import the .vo file? If not, what would be the best way to proceed, if this is at all possible? Thanks.

view this post on Zulip Karl Palmskog (Dec 06 2023 at 09:04):

I have only anecdotal evidence when I accidentally mixed MC1 and MC2 locally - it broke down very quickly during compilation (reuse of .vo file isn't possible since Coq stores hashes of dependencies)

view this post on Zulip Pierre Roux (Dec 06 2023 at 09:06):

I wouldn't expect anything either. The only robust solutions seem to port the old development to MC 2 or (worse but maybe easier if it is tiny) the new one to MC 1. Note that porting to MC2 can be trivial or very easy if the development is not using many structures.

view this post on Zulip Pierre Jouvelot (Dec 06 2023 at 09:15):

Thanks @Karl Palmskog @Pierre Roux for the fast and somewhat expected answer :smile:

Last updated: Jul 15 2024 at 21:02 UTC