• Use virtualenv to keep Cozy and its dependencies isolated from the rest of your system.
• PyCharm is a good choice for developing and debugging. It has many useful features:
  • Set breakpoint: conditional or not
  • Sometimes failed assertions / exception might not be caught, move the code a bit and place a manual breakpoint
  • Watcher is awesome
  • Stepping is more reliable
  • Find usage

The tests folder contains tests written with Python's unittest library. Run them with

$ python3 -m unittest -b tests/*.py

(The -b flag "buffers" output so that Python only shows output from failing tests.)

The cozy/synthesis folder contains the core synthesis algorithm and some useful additions.

The cozy/codegen folder implements source code generation for C and Java.

A pre-commit hook is a script that runs when you run git commit. The commit aborts if the script fails. This pre-commit hook runs a linter and all the unit tests:

$ cat .git/hooks/pre-commit

#!/bin/bash
./lint.sh && python3 -m unittest -fb tests/*.py

$ cat lint.sh 
#!/bin/bash
cd "$(dirname "$0")"

if [[ "$1" == "" ]]; then
    ARGS="$(find cozy tests -name '*.py' -not -name 'parsetab.py')"
else
    ARGS="$@"
fi

# http://flake8.pycqa.org/en/latest/user/error-codes.html
# https://pycodestyle.readthedocs.io/en/latest/intro.html#error-codes
echo "Running flake8..."
exec flake8 \
    $(fgrep -- '--select' .travis.yml) \
    $ARGS
echo "Done!"

There are multiple notions of "equality" between values and between expressions in Cozy. Value equality is documented in value_types.py.

Expressions have three different kinds of equality: syntactic equality, alpha equivalence, and semantic equality.

• syntactic equality means they are the same expression, right down to the names of variables
• alpha equivalence means they are the same expression, but variables can be renamed if it doesn't affect the meaning of the expression
• semantic equivalence means the expressions produce the same output on all inputs

In the Cozy Python code, == on Exp objects implements syntactic equality (but ignores type information). alpha_equivalent tests for alpha equivalence (but also ignores type information). valid can be used as a partial decision procedure for semantic equality (the task is undecidable, unfortunately). Usually this is written valid(EDeepEq(e1, e2)). For expressions with non-collection types, valid(EEq(e1, e2)) accomplishes the same thing.

1. Locate the root cause for non-optimality: which individual program construct in spec leads to inefficient code? This is difficult to answer by deduction. The best way to find this out is through experiments: have a hypothesis about which part might be problematic, simplify all other parts in your spec to single it out. Test the performance or simply stare at the (much shorter) generated code.
2. Manually figure out how this minimal case is supposed to be synthesized efficiently. Try to extract some general rules or generic path of search.
3. Hook into Cozy in a debugger. See how it deal with relevant expressions in practice.