coqide-无法从同一文件夹加载模块 [英] coqide - can't load modules from same folder

问题描述

我无法加载CoqIde中同一文件夹中的模块。

我正在尝试从Software Foundations加载源，我正在文件夹中运行coqide包含带有 coqide 或 coqide ./的SF源，然后在打开并运行文件后，我得到了错误：

 错误：在加载路径
   
 
 
在此行中：
 需要导出多边形。 
  
其他所有 require 命令都相同
 
 
 
那么您如何将程序从SF加载到coqide中？
解决方案
如果需要将.v文件编译为.vo文件，并将其目录添加到加载路径中。要编译它们，请在命令提示符下运行 coqc< file-path> 。要将文件目录添加到CoqIde的加载路径中，可以在.v文件的开头插入 Add LoadPath< directory-path>。行。 
 
I can't load modules that are in same folder in CoqIde.

I'm trying to load sources from Software Foundations, I'm running coqide in folder that contains SF sources with coqide or coqide ./, then after opening and running the file, I'm getting this error:
Error: Cannot find library Poly in loadpath
in this line:
Require Export Poly.
and it's same for every other require commands.

So how are you people loading programs from SF into coqide ?
解决方案
You need to compile the .v files into .vo files and add their directory to your load path if you're going to require them. To compile them, run coqc <file-path> in the command prompt. To add the files' directory to your load path in CoqIde, you can insert the line Add LoadPath "<directory-path>". at the beginning of the .v files.

                        
这篇关于coqide-无法从同一文件夹加载模块的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！