Как работает сценарий оценивания серии 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

Что мне не хватает?


coq logical-foundations
person Tejas Shah    schedule 28.10.2020    source источник

Ответы (1)


arrow_upward
0
arrow_downward

С этим особо ничего не поделаешь, потому что эти упражнения нужно оценивать вручную. Если вы сдаете это в качестве домашнего задания, вам придется перепроверить, что вы сделали все ручные упражнения самостоятельно. Если вы учитесь сами, вы можете поставить себе фиктивную оценку, изменив None. на Some (1, ""%string)..

person Li-yao Xia    schedule 28.10.2020
comment
Я изучаю этот курс в университете и подумал, что сценарии оценивания извлекают комментарии из оцениваемых вручную упражнений, чтобы преподавателям не нужно было прокручивать всю документацию и текст, чтобы найти то, что написали студенты. Я думаю, что это их предполагаемое поведение. Я не знаю, как заставить это работать. - person Tejas Shah; 29.10.2020
comment
У учителей есть свои сценарии. Те, которые приходят с вашими домашними заданиями, должны помочь вам отслеживать ваш прогресс, а ручные упражнения не отслеживаются. - person Li-yao Xia; 29.10.2020