coqide-无法从同一文件夹加载模块 | 无法从同一文件夹加载模块

本文介绍了coqide-无法从同一文件夹加载模块的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！

问题描述

我无法加载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-无法从同一文件夹加载模块的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！