Stream: Coq users

Topic: Software Foundations - QuickChick TImp.v - fails to find QC


view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip jco (Jun 20 2020 at 16:28):

yeah hm it seems I lost the monadic G A stuff, at the very least

view this post on Zulip Enrico Tassi (Jun 20 2020 at 16:54):

You probably passed a wrong -Roption to coq_makefile

view this post on Zulip 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.

view this post on Zulip 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: Feb 08 2023 at 23:03 UTC