jco (Jun 20 2020 at 15:57): jco (Jun 20 2020 at 15:57):My coq version is 8.11.2, and I had to use coq_makefile to make a new makefile for this project. I mention this because it's possible I messed up!
When I run a make command, I get the following warning: *** Warning: in file TImp.v, library QC.QC is required and has not been found in the loadpath!
There is a QC.v file present, though. The line that creates the warning: From QC Require Import QC. I've noticed there have been some errors in this module (perhaps bitrot with newer versions of Coq?), so I think there may just be a newer more correct way to do it.
FWIW, I'm just using the software foundations downloaded from the website (the makefile was built with coq 8.11.1). I extracted the files into a directory and ran make (well, after recreating the makefile to get rid of another warning)
Thanks in advance for any help!
jco (Jun 20 2020 at 16:17):I noticed there is a _CoqProject file with the contents -Q . QC, which seems potentially related but I tried removing it and nothing changed, so no clue
jco (Jun 20 2020 at 16:20):Error in building when it gets to the file:
File "./TImp.v", line 12, characters 23-25:
Error: Cannot find a physical path bound to logical path matching suffix
<> and prefix QC.
jco (Jun 20 2020 at 16:25):When I try to combine in Coqtail (vim), I get this error: The file /Path/To/Software Foundations/qc/QC.vo contains library
Top.QC and not library QC.QC which leads me to believe that this isssue is that QC.v is missing something now or something
jco (Jun 20 2020 at 16:26):I guess I can just get rid of the import and see where the file starts messing up...
jco (Jun 20 2020 at 16:28):yeah hm it seems I lost the monadic G A stuff, at the very least
Enrico Tassi (Jun 20 2020 at 16:54):You probably passed a wrong -Roption to coq_makefile
Enrico Tassi (Jun 20 2020 at 16:55):The original makefile should have a comment, in the header, with the options that were used to generate it.
jco (Jun 21 2020 at 02:26):That worked! Sigh, I should really prioritize understanding how all of this stuff gets built. Thanks again
Last updated: Apr 20 2024 at 00:02 UTC