Getting Started

For the twenty-sixth class, we are going to take a look at some of the REPLICA data and benchmarks, to get a sense of what the user-collected data looks like, and how these users interact with the Coq proof assistant.

Luckily, there is no installation required for this! Hopefully that is a nice relief after some of the installation troubles recently (sorry about that).

You can find the exercise we will do together in class below.

Let's Hack!

Let's Hack!

During class, after diving into groups, we will take a look at the data repository for the REPLICA paper. Any workflow for exploring the data is fine, but here is one suggested workflow to get you started, with some questions to discuss with your group along the way:

  1. Read the README to get a sense of the repository organization.
  2. Take a look at the benchmarks. Is there anything you find interesting or informative about the benchmarks?
  3. Take a look at the list of all changes identified. Do you see anything you find interesting or informative about the changes?
  4. Think about what other questions you might ask about the data not answered by the study. Do you have enough information to answer those questions, given enough time? How might you go about doing so?
  5. Poke around at the analysis scripts. Do you understand what is going on? How might you go about writing scripts to answer the questions you identified about the data in the previous step?
  6. How might you automate more of this workflow, if at all?
  7. If time allows, spend some time cloning the repository and running the scripts, possibly modifying them if interested. Or, spend some time poking around at the raw data or at other Git commits. What did you learn from this?

The only graded part will be answering the following discussion question (to be posted in this thread, listing all group members in your response): What did you learn from exploring the data that you did not learn from reading the paper? How might this influence work that you might do in this space, whether that work is another user study, an analysis of the existing data, or the design or improvement of a tool addressing user needs?

You can do this on your own if you cannot make it to class, or enter a Zoom breakout if you're remote. Let me know if you can't attend, but would like me to find you a partner or make an exception.

<< Previous | Class Schedule | Next >>