Clever Geek Handbook

Coq makefile "Top". Prefix

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

+3


source to share


2 answers


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

.



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

.

+2


source


This is really annoying. To avoid this kind of annoyance, always start yours _CoqProject

with string enumeration options:

-Q . MyProject


To note: the parameters that you can put on the first line of yours _CoqProject

are listed when called coqtop -help

.

+1


source






More articles:


All Articles