Mukesh Tiwari (Mar 03 2023 at 11:50): Mukesh Tiwari (Mar 03 2023 at 11:50):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
Matthieu Sozeau (Mar 03 2023 at 12:50):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
Mukesh Tiwari (Mar 03 2023 at 13:47):@Matthieu Sozeau Thanks! I assume I should downgrade my Coq version to 8.16 and then install MetaCoq?
Matthieu Sozeau (Mar 03 2023 at 14:01):You should rather install the MetaCoq 8.16 branch if you want to run the code. Keeping Coq 8.16 or 8.16.1
Mukesh Tiwari (Mar 03 2023 at 14:33):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?
Yannick Forster (Mar 03 2023 at 14:33):What do you mean by code extraction?
Mukesh Tiwari (Mar 03 2023 at 14:38):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?
Yannick Forster (Mar 03 2023 at 14:41):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/
Yannick Forster (Mar 03 2023 at 14:41):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
Yannick Forster (Mar 03 2023 at 14:42):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 :)
Mukesh Tiwari (Mar 03 2023 at 14:44):Thanks @Yannick Forster !
Yannick Forster (Mar 03 2023 at 14:44):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
Notification Bot (Mar 04 2023 at 10:46):Mukesh Tiwari has marked this topic as resolved.
Meven Lennon-Bertrand (Mar 06 2023 at 10:37):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?
Yannick Forster (Mar 06 2023 at 10:44):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