Run `make HW_filename Test.vo` Command

While working on your homework, you can run the make command to generate a report showing the results of all test cases. The detailed steps are given below:

1. Open a terminal tab in VSCode

   

2. cd to the directory containing the source file you are working on

   • For HW1, you are working on Basics.v, and it's located under lf/full; therefore, the first step is to cd lf/full

3. Issue make <HW_filename>Test.vo command, where <HW_filename> is the filename that you are working on

   • For HW1, you are working on Basics.v, thus, the command will be make BasicsTest.vo
   • Note that in the future homework, you might need to work on multiple files; in that case, you will need to run make <HW_filename>Test.vo command for each of them

4. If there is any syntax/grammar error in your code, the error will be printed, and you need to fix them and re-run the make command; if there is no error, a report will be printed

Reading the report

The report shows the detail for each test case, as shown in the screenshot below, it contains the name of the test case, the maximum points of that test case, and the result of that test case.

The result can be any of the following:

• 'Closed under the global context', if it is complete
• 'MANUAL', if it is manually graded
• A list of pending axioms, containing unproven assumptions. In this case the exercise is considered complete, if the axioms are all allowed.

For HW1, there are no axioms allowed, thus, for the screenshot shown below, none of the test cases is considered complete.

And for the screenshot shown below, the test cases are considered complete,
since the result section is showing Closed under the global context

And the example (from HW1) below shows the test case, negation_fn_applied_twice, is a manually graded exercise.