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!
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
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.
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
I guess I can just get rid of the import and see where the file starts messing up...
yeah hm it seems I lost the monadic
G A stuff, at the very least
You probably passed a wrong
The original makefile should have a comment, in the header, with the options that were used to generate it.
That worked! Sigh, I should really prioritize understanding how all of this stuff gets built. Thanks again
Last updated: Feb 08 2023 at 23:03 UTC