Coq生成文件"Top".字首

本文介绍了Coq生成文件"Top".字首的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！ 问题描述

我正在使用自动Coq 8.5生成文件生成器.该makefile在所有模块的前面加上"Top". . 现在，假设您通过make运行了许多文件，然后想要在IDE中更改/调试某些文件. 然后，令人讨厌的事实是Coq抱怨它找不到已编译的其他文件，因为在IDE中它假定名称没有"Top"前缀. 我试图调整makefile以摆脱该前缀.但是我总是以make的错误信息结尾. 有人可以告诉我如何在make中删除"Top"前缀，还是告诉IDE使用"Top"前缀.

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.

推荐答案

您可以使用以下参数coqide -R . Top启动CoqIDE.

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

这将消除以下错误Error: The file ..../Logic.vo contains library Top.Logic and not library Logic.