makefile - 软件基础-自动评分

Question

为了学习Coq，我从here下载了Benjamin Pierce的电子书软件基础，​​并提取了其中的内容。我现在开始通过直接在Vim中编辑文件来完成Basics.v中的练习。

我想自动为我的答案评分(例如，根据时间跟踪我的得分)。

为此，我按照coqc中给出的顺序针对每个.v文件运行了Makefile。因此，我是now able to invoke，例如coqtop -batch -l BasicsTest.v。

但是，尽管这报告了该章的可用分数，但并未报告我的分数。 (我正在本章的中间，并且相信到目前为止我的答案是正确的，因为coqtop -batch -l Basics.v的执行没有错误。)

我怀疑我忽略了Make或Coq的调用，该调用到目前为止会为我的答案产生分数。如果是这样，那是什么？

Answer 1

在当前版本的Software Foundations中，BasicsTest.v不会生成评分。您可以逐步了解它的作用:只需简单地进行练习，执行一些基本检查并报告其结果。但是，不会根据这些检查的结果生成分数。

如果您的定义和证明是完整的(例如，不是Admitted)，并且Coq的类型检查器接受了它们，则您可以有合理的信心，答案是正确的，除非您的开发中有某些东西破坏了Coq的逻辑一致性(在此早期阶段不太可能)或您偶然发现了一个错误(也是极不可能的)。