LF 系列的评分脚本如何用于手动评分练习？答案

【问题标题】：How does the grading script of the LF series work for manually graded exercises?LF 系列的评分脚本如何用于手动评分练习？
【发布时间】：2020-10-28 16:59:52
【问题描述】：

我试图弄清楚 LF 测试脚本在从终端运行时如何输出手动评分的作业。例如，如果您查看Induction.v 有一个名为plus_comm_informal 的练习，我正在尝试获取测试脚本InductionTest.v 来获取我编写的cmets 或内容。所以我做了以下尝试猴子调试。

(** **** Exercise: 2 stars, advanced, especially useful (plus_comm_informal) 

    Translate your solution for [plus_comm] into an informal proof:

    Theorem: Addition is commutative.

    Proof: (* Let's see how this works! 1*)
    Let's see how this works! 2
*)

(** Let's see how this works! 3 *)

(* Let's see how this works! 4 *)

(* Do not modify the following line: *)
Definition manual_grade_for_plus_comm_informal : option (nat*string) := None.
(** [] *)

我保存了文件。然后我用coqc -Q . LF .\Induction.v编译文件，然后用coqc -Q . LF .\InductionTest.v运行测试文件

它的输出并没有给出我在手动评分练习中通过的任何 cmets。终端输出的相关部分如下。

-------------------  plus_comm_informal  --------------------

#> Manually graded: plus_comm_informal
Advanced
Possible points: 2
Score: Ungraded
Comment: None

我错过了什么？

【问题讨论】：

标签： coq logical-foundations

【解决方案1】：

这方面没什么可做的，因为这些练习必须手动评分。如果您将其上交家庭作业，则必须仔细检查您是否自己完成了所有手动练习。如果您正在自学，可以通过将None. 更改为Some (1, ""%string). 来给自己一个虚拟成绩

【讨论】：

我在大学做这门课程，我认为评分脚本会在手动评分练习中提取 cmets，这样教师就无需滚动浏览所有文档和文本来查找内容学生们写了。我认为这是他们的预期行为。我不知道如何让它发挥作用。
教师有自己的剧本。作业附带的那些是为了帮助你跟踪你的进度，不跟踪手工练习。