Willard Rafnsson (Apr 06 2022 at 02:03): Willard Rafnsson (Apr 06 2022 at 02:03):Hi, I have a .v file generated by Why3's Coq driver. I am trying to step through the file using proof-general in emacs. However, this fails already at the first line, with Error: Unable to locate library BuiltIn. (While searching for a .vos file.). I know where to locate the missing files on my system (~/.opam/default/{.opam-switch/sources/why3.1.4.1/lib,lib/why3}/coq, opt/GNAT/2021/libexec/spark/share/why3/libs/coq/). However, I do not know how to make proof-general (coqtop) aware of these files. Any ideas of how I proceed?
Willard Rafnsson (Apr 06 2022 at 03:04):Progress: If I put -R ~/.opam/default/lib/why3/coq/ Why3 into the _CoqProject file, then it works; I can step through the .v file. This is because the indicated directory contains .vo files, i.e. compiled libraries (Why3 people: it was quite frustrating to have to discover what to add to _CoqProject, and that it should be named Why3, through trial and error). Next question: I would like to instead use the files from ~/opt/GNAT/2021/libexec/spark/share/why3/libs/coq/ (since that is what gnatprove will use, which ultimately checks my proof; if why3-coq becomes different from what ships with gnatprove, then proof checking might fail in emacs or by gnatprove). However, there are no .vo files in ~/opt/GNAT/2021. Is there a way to load .v files instead of .vo files?
Guillaume Melquiond (Apr 06 2022 at 06:37):As for the last question, the answer is no. Regarding ProofGeneral, if you are launching it from Why3, then Why3 is supposed to take care of initializing it properly. But if you are launching it by hand, then using _CoqProject is a solution. Another solution is to add (setq coq-load-path ((".../lib/why3/coq/" "Why3"))) to your Emacs' configuration.
Last updated: Oct 13 2024 at 01:02 UTC