Iteration 29

[ttuegel]

Iteration 29

19 August 2020 to 02 September 2020

Iteration 29 Milestone

Plan

• Performance
  • Simplify right-hand side of claims #1278: Simplify right-hand side of claims
• Bugs
  • Symbolic rules for SET.in #2020: Symbolic rules for SET.in
  • Every leaf of a proof tree should be explicitly "proven" or "stuck" #2021: Every leaf is "proven" or "stuck"
  • Error Failed to decide predicate for in_keys #2075: Failed to decide predicate
  • Unit tests should not invoke SMT solver #2078: Unit tests should not invoke SMT solver
  • ErrorDecidePredicateUnknown is not actually an error #2072: ErrorDecidePredicateUnknown is not actually an error
  • Lemma related to set "in" not always applied #1725: Lemma related to SET.in not always applied
  • Rewriting multiple items in a KSequence causes a crash #2023: Rewriting multiple items in a KList causes a crash
• User experience
  • Apply function definitions with unification instead of matching #1630: Apply function definitions with unification instead of matching
  • Evaluating functions with partial arguments #1978: Evaluating functions with partial arguments

Engineering practices

Appetites

Our appetite for a task is the amount of time we are willing to spend on it. We use labels for appetites:

• S (t < 1d): small tasks, up to 1 day
• M (t < 2d): medium tasks, up to 2 days
• L (t < 4d): large tasks, up to 4 days

Whenever possible, we prefer to break up large tasks into smaller units.

Tasks usually have two phases:

• Uphill: initial phase, discovering requirements and searching for a solution.
• Downhill: final phase, implementing the solution found in the first phase.

The downhill phase may not be monotonic; it can be punctuated by smaller "uphill" regions.

When the appetite for a task is exceeded, this is a checkpoint to decide if or how we want to continue with the task. If the task is still moving uphill, we will probably stop working on it. If we have identified a partial solution, we may try to reduce the scope of the task.

Code review and refactoring

Every pull request is reviewed by another member of the team. We take time during the daily meeting to check that every "ready" pull request has an assigned reviewer. Studies suggest that code review works best when pull requests are no more than 300-400 lines of code. Reviewing a pull request of that size should take 30-60 minutes, depending on the complexity of the code. After 60 minutes, it is difficult for the reviewer to maintain focus.

Whenever possible, we try to break up larger pull requests to fit within this limit. We also try to separate refactoring from behavioral changes to the code. Refactoring is much easier to review, but separating refactoring from behavioral changes also makes it easier to track down regressions.

The primary reviewer for a pull request is also expected to carry out refactoring or clean-up where they feel it is appropriate. For small pull requests, these additional changes can simply be pushed to the pull request branch before merging, but for large changes, opening a new pull request is appropriate. There are several reasons we do this:

1. It helps keep the code clean. Clean code is maintainable; it's easier to come back to later. We often don't even realize that some part of the code is awkward until someone has to change it later, so it's not always enough just to look at the code.
2. If we don't make time for clean-up, it won't happen: there is always something else to do.
3. It spreads knowledge. The reviewer will understand the new code better than if they had only read and reviewed it.
4. It improves the quality of the code review. If some part of the code is difficult to understand or review, refactor it first!

Domain-driven design

The goal of domain-driven design is to build a shared mental model between developers and domain experts (users, verification engineers, theorists).

More here: https://runtimeverification.slack.com/archives/CC360GUTG/p1580937544199700

Test-driven development

The basic workflow of test-driven development is:

1. Write a failing test.
2. Write just enough code to pass the test.
3. Refactor?

The purpose of the workflow is to ensure that there is test coverage for every decision we make about what the code should do. We want 100% test coverage of our intent, not necessarily 100% test coverage of lines-of-code. The workflow is strict because we tend to make many decisions automatically and unconsciously, but we need to capture those same decisions in the tests.

Aside from this workflow, branch protections are enabled so that every pull request passes the full test suite before merging to the master branch.