如何解决LF系列的评分脚本如何用于手动评分练习?
我试图弄清从终端运行时LF测试脚本如何输出手动评分的作业。
例如,如果您查看Induction.v
,有一个名为plus_comm_informal
的练习,我正在尝试获取测试脚本,InductionTest.v
来拾取我写的评论或内容。
因此,我进行了以下尝试以进行调试。
(** **** 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
该命令的输出不会给我任何我在手动分级练习中传递的评论。 终端输出的相关部分如下。
------------------- plus_comm_informal --------------------
#> Manually graded: plus_comm_informal
Advanced
Possible points: 2
Score: Ungraded
Comment: None
我想念什么?
解决方法
与此无关,因为这些练习必须手动评分。如果要上交作业,则必须再次检查自己是否完成了所有手动练习。如果您正在自学,则可以将None.
更改为Some (1,""%string).
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。