- 1.I'm seeing a syntax error in a docstring where there is no annotation. What gives?
You may be using an older version of scribble. Earlier scribble allowed annotations without a leading
invariant x > 0;instead of
#invariant x > 0. However we found that since some of the keywords we use (e.g.
define) can occur in normal docstrings, sometimes scribble can get confused and try and treat something that is not an annotation as an annotation. To solve this problem we made the
#required. So try to upgrade scribble to the latest version, and make sure all your annotations start with
2. I'm getting an error "TypeError: Variable ... is defined in the new context in ... but used in an old() expression"