Open janvrany opened 5 months ago
I recommend focusing on one topic per PR. This particular change would be named something like "Use upstream Sprite annotation syntax (/@…/)", and cherrypick this commit, change the tests, and remove the ⟦...⟧.
OK, no problem.
Are you suggesing to depart from the upstream syntax here?
Yes.
Wait, how is this any different? I am looking at #word...
Ah, my bad. IIRC this has not been so in the early versions of PP, will drop that change.
Are you suggesing to depart from the upstream syntax here?
Forget it, I'll deal with that differently some time in the future.
Ok, this is excellent.
Now the next question is how to merge such things. Because if we merge into pure-z3
, it will break all the branches. I think this simply means we should prioritize merging that whole zoo-of-branches into pure-z3
asap.
We can drop last commit (removing support for [[ ]]) and add it later, once the rest is merged, or the other way round, Up to you.
This PR scratches the worst of my itches when writing Sprite by hand. Still, there's more to fix (#193 and things I already forget)