Update to MetaCoq 1.3

[womeier]

I was looking into extracting the counter module to concordium, using our Wasm backend for CertiCoq.

CertiCoq is currently on MetaCoq 1.3, which ConCert doesn't seem to work with.

Do you already have plans to update?

[4ever2]

I already started looking at updating to MetaCoq 1.3. However, I ran into a problem that looks like a MetaCoq bug. I haven't had time yet to identify the exact cause of the problem.

[spitters]

@4ever2 we should get ConCert in MetaCoq CI...

[spitters]

Here's what we need to do. Let's find a local Nix expert... https://coq.zulipchat.com/#narrow/stream/237658-MetaCoq/topic/CI/near/292131799

…

On Tue, Apr 9, 2024 at 9:17 AM 4ever2 ***@***.***> wrote: I already started looking at updating to MetaCoq 1.3. However, I ran into a problem that looks like a MetaCoq bug. I haven't had time yet to identify the exact cause of the problem. — Reply to this email directly, view it on GitHub <#242 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AABTNTWJTB7EYBW2QDIDETTY4OI2FAVCNFSM6AAAAABF54QKOOVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDANBUGMYDCOBTGE> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[womeier]

I already started looking at updating to MetaCoq 1.3. However, I ran into a problem that looks like a MetaCoq bug. I haven't had time yet to identify the exact cause of the problem.

@4ever2 It seems you have a version that works with MC 1.3 (without support for the elm extraction, that's no big deal of course).
Could you push that to a branch?
Things break at various places when I update to MC 1.3.

[womeier]

I have a version of ConCert now (with a bunch of things commented out), that compiles with MetaCoq 1.3.

Extracting the counter smart contract works, but I can't yet compile the extracted rust project as I'm not sure how to set up the required concordium libraries.
Could you give me a pointer on which versions of which packages I should install?

Running cargo build in extraction/tests/extracted-code/concordium-extract/counter-extracted gives the following error:

error: failed to select a version for the requirement `concordium-std-derive = "^2.0"`
candidate versions found which didn't match: 6.0.0
location searched: crates.io index
required by package `concordium-std v2.0.0`
    ... which satisfies dependency `concordium-std = "^2.0.0"` of package `concert-std v0.1.0 (/home/wolfgang/ProjectsUni/Compilerstep/smart_contracts/ConCert/extraction/tests/extracted-code/concordium-extract/concert-std)`

It seems I need version 2.0.0, which is not available via crates.io, is that what you currently use?

[spitters]

@womeier I seem to recall you made progress on this. What's the current status?

[womeier]

I commented out some proofs and tests, to make the counter module extraction work with MetaCoq 1.3, I don't think the other smart contracts work.

These are my changes:
womeier/coq-rust-extraction@f113dff
womeier@cf5d7d8