CODEWITHSUNDEEP
coqide
Cryptostasis
Cryptostasis

Reputation: 1216

Coq makefile "Top." Prefix

I am using the automatic Coq 8.5 makefile generator. This makefile prefixes all modules by "Top." . Now let's say you run a lot of files by make and then want to change/debug some file in the IDE. Then the annoying fact is that Coq complains it cannot find the compiled other files, because in the IDE it assumes the names without the "Top" prefix. I tried to tweak the makefile to get rid of this prefix. But I always ended in some error message of the make. Can someone show me either how to remove "Top" prefix in make or tell the IDE to use the "Top" prefix.

Upvotes: 4

Views: 637

Answers (2)

Daco Harkes
Daco Harkes

Reputation: 446

You can start CoqIDE with the following arguments coqide -R . Top.

This will get rid of the following error Error: The file ..../Logic.vo contains library Top.Logic and not library Logic.

Upvotes: 3

Zimm i48
Zimm i48

Reputation: 3081

This is annoying indeed. In order to avoid that kind of annoyance, always start your _CoqProject with a line listing options:

-Q . MyProject

To note: the options you can put on the first line of your _CoqProject are the ones listed when calling coqtop -help.

Upvotes: 1

Related Questions