6

In order to learn Coq, I downloaded Benjamin Pierce's ebook Software Foundations from here, and extracted the contents. I am now starting to work through the exercises in Basics.v, by editing the file directly in Vim.

I would like to automatically grade my answers (e.g. to track my point score against time).

In preparation for this, I ran coqc against each of the .v files in the order given in the Makefile. As such, I am now able to invoke, e.g. coqtop -batch -l BasicsTest.v.

However, although this reports the available number of points for that chapter, it does not report my score. (I am mid-way through the chapter, and am confident my answers so far are correct, as coqtop -batch -l Basics.v executes without errors.)

I suspect I have overlooked an invocation of Make or Coq that will produce a points score for my answers so far. If so, what is it?

  • 2
    Pretty much everyone uses an interactive editor to solve Coq problems rather than a text editor together with the batch mode. You may want to look into coqide / proofgeneral. It'll make your life way easier. – gallais Aug 02 '17 at 12:23
  • @gallais, thanks for trying to help :) My recollection of CoqIDE is that it lacked a good text editing interface. I spent some time with Proof General a while ago, and may return to it. I liked what it was trying to achieve, but it still felt cumbersome compared to using a text editor and Bash. My subjective impression was that it made Emacs slower and more prone to crashing :( –  Aug 02 '17 at 12:47

2 Answers2

13

The autograder is currently incomplete. We hope to finish it over the next few months and will make it available when we do. But as Rob says it's really not telling you much more than what you get by running BasicsTest.v in the current beta version.

UPDATE December 2018: The autograder is finished. We haven't packaged it (except for the actual tester files like BasicsTest.v) for public distribution, but we're happy to give access to the Git repo to instructors who want to use it.

Benjamin Pierce
  • 497
  • 2
  • 10
  • 7
    Assuming this is the real Benjamin Pierce, thank you for creating such inspiring educational materials, and for making them available to people outside your department. It means a lot! Looking forward to the completed autograder. Feel free to update this answer once it is published. Thanks again :) –  Aug 02 '17 at 13:39
3

BasicsTest.v does not generate a grade in the current version of Software Foundations. You can step through it and see what it does: it simply goes through the exercises, performs some basic checks and reports their results. However, scores are not generated based on the results of these checks.

If your definitions and proofs are complete (e.g., not Admitted) and Coq's typechecker accepts them, you can have reasonable confidence that the answers are correct, unless something in your development breaks the consistency of Coq's logic (very unlikely at this early stage) or you stumbled upon a bug (also extremely unlikely).

Rob Blanco
  • 296
  • 1
  • 5