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 we should get ConCert in MetaCoq CI...

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.

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?

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

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