I have a test_1.v file in the test1 folder, and compile test_1.vo with coqc. I want to reference the test_1.vo library in test_2.v in the test2 folder: “Require Import test_1.”, but compile test_2 with coqc. v error: Unable to locate library test_1. Why is this?
As soon as you have a project with several files, you should create a _CoqProject file and use coq_makefile to generate a Makefile that you can use to compile your project. coqc is not really meant to be used by hand.
Here, in addition of having several files, you have several folders. This makes it all the more important to use such a setup.
See documentation here: https://coq.inria.fr/refman/practical-tools/utilities.html#building-a-coq-project
1 Like