Stream: Coq users

Topic: compiling a project


view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:33):

I'm trying to compile a project by coqc-ing the .v files one by one. Works fine for the first file, but the second cannot find the first as an import:

skraeling@moria /cygdrive/d/dev/coq/coq-proofs/Reciprocity
$ coqc Accumulation.v
File ".\Accumulation.v", line 1, characters 15-45:
Error: Cannot find a physical path bound to logical path matching suffix
Reciprocity.Reciprocity.

Is there a way I can tell coqc where to look?

view this post on Zulip Darij Grinberg (Feb 18 2022 at 21:35):

oh figured this one out
there was a ./configure


Last updated: Jan 29 2023 at 04:05 UTC