Stream: Coq users

Topic: Multiple files in Coq IDE


view this post on Zulip Gergely Buday (Jul 13 2020 at 13:15):

I am to run Coq scripts. I loaded a file into Coq IDE but it stops at using an identifier defined in another .v file.

The first file imports the second via

Require Import

Should I do something special so that Coq IDE would load the second .v file and recognize that identifier.

Should I first run that second file through Coq and save a compiled version of it?

view this post on Zulip Karl Palmskog (Jul 13 2020 at 13:23):

CoqIDE needs files that you load to be already compiled to .vo format. This can be accomplished directly via coqc or indirectly via coq_makefile for the file you need to load.

view this post on Zulip Gergely Buday (Jul 13 2020 at 13:25):

Thanks

view this post on Zulip Gergely Buday (Jul 14 2020 at 07:00):

I compiled the dependency file into .vo object file with coqc.

Still, when I open the first file I stuck at an identifier that is from the dependency file.

What did I miss?


Last updated: Jan 28 2023 at 06:30 UTC