4ever2
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...
Hi, ConCert is made up of three layers (projects) a smart contract layer, an embedding layer, and an extraction layer. We have already been talking about moving some parts of...
Elm and Rust extraction are now released in the Coq opam repository.
This https://github.com/MetaCoq/metacoq/commit/fa4b728f2ecd74f7503d682bccfe31facc8d7747 commit fixes the issue. Thanks for the help. I see that the commit was not included in the 1.3.2 release. This issue is blocking upgrading a few of...
SSProve 0.3.0 release is available now, it should be compatible with MC 2.5.0.
> This is something we inherit from C.J.'s VsCoq 1, I think that VSCoq 2 also uses the same file; maybe we could sync the effort on Zulip to improve...
> * The MC-dev build is failing, but I do not think it is due to changes that I introduced. Is it possible to rebuild main and see if it...
The problem with mathcomp master is now fixed. > * I would suggest merging this into a new branch e.g. `towards-nominals`, so that all breaking changes can be introduced at...
> * Does the `loc_rel` invariant need to be fixed? The idea is cool, but it is not used anywhere in this codebase and the current automation/lemmas for it looks...
We are not merging into main yet, and many other breaking changes are coming in the next PRs, so let's wait with the documentation. Lasse also approved the changes, so...