Hi everyone,

I am just copy and pasting the code from this repo in my editor (VSCode). But when I reach the line `From MetaCoq.TemplatePCUIC Require Import TemplateToPCUIC PCUICToTemplate`

I get this error (I am using Coq 8.16.1):

```
Error: Cannot find a physical path bound to logical path
TemplateToPCUIC with prefix MetaCoq.TemplatePCUIC.
opam list show the following libraries:
coq-metacoq 1.1.1+8.16 A meta-programming framework for Coq
coq-metacoq-erasure 1.1.1+8.16 Implementation and verification of an erasure procedure for Coq
coq-metacoq-pcuic 1.1.1+8.16 A type system equivalent to Coq's and its metatheory
coq-metacoq-safechecker 1.1.1+8.16 Implementation and verification of safe conversion and typechecking algorithms for Coq
coq-metacoq-template 1.1.1+8.16 A quoting and unquoting library for Coq in Coq
coq-metacoq-translations 1.1.1+8.16 Translations built on top of MetaCoq
mukeshtiwari@dhcp-10-248-123-234 Dlog-zkp % coqtop -v
The Coq Proof Assistant, version 8.16.1
compiled with OCaml 4.14.1
```

Does the code compile? If yes, it's likely about vscoq using the wrong coq installation

Hi Mukesh, I think you're mixing versions, the code in the repo requires the latest 8.16 branch of MetaCoq rather than the 1.1.1 package

@Matthieu Sozeau Thanks! I assume I should downgrade my Coq version to 8.16 and then install MetaCoq?

You should rather install the MetaCoq 8.16 branch if you want to run the code. Keeping Coq 8.16 or 8.16.1

I can install the MetaCoq 8.16 branch but my ultimate goal is to use MetaCoq in my project for code extraction to see, and get some feeling, how it compares to the normal Coq extraction. Can I do this without installing MetaCoq 8.16 branch?

What do you mean by code extraction?

Say I have a Coq development and I can extract a Coq function into OCaml using the extraction mechanism build into the Coq environment. Now I am wondering if I can do the same, extracting OCaml, using the MetaCoq library, or did I get it completely wrong?

Verified extraction isn't part of MetaCoq, and overall still work in progress. There is no release, and I'm not sure whether the current state of the code compiles. If you want, you can give it a try here: https://github.com/yforster/coq-malfunction/

There are installation instructions, but I think they are outdated. You might get lucky by replacing unshadowing by unshadowing-rebased in the instructions, but I'm not sure

Overall, my recommendation would be that if you want to use extraction based on MetaCoq, you need to wait a bit until a first release :)

Thanks @Yannick Forster !

The file you liked above from the MetaCoq repo just runs erasure. The result is a lambda_box term, which is still relatively far away from an OCaml program and which cannot be executed

Mukesh Tiwari has marked this topic as resolved.

Yannick Forster said:

The file you liked above from the MetaCoq repo just runs erasure. The result is a lambda_box term, which is still relatively far away from an OCaml program and which cannot be executed

Can't you already go through CertiCoq, though? Of course, this is not compilation to OCaml, but this means you can already compile these erased terms to (C) code that can run. Or am I mistaken?

Yes :) Documentation might be sparse and some bugs might occur, but you can get C code

Last updated: Jun 03 2023 at 17:29 UTC