[Agda] Known inconsistency not fixed in release for one year

[Paolo G. Giarrusso]

Hi all,

one year ago, a trivial soundness bug was discovered in Agda, fixed the day
after with a one-line fix (https://code.google.com/p/agda/issues/detail?id=843).
The bug makes programs return wrong results, possibly with the wrong type. I
think this issue is critical (if I'm wrong I'd like to learn why). But to this
day, the patch has never been included in a stable release. Yesterday, the bug
was found again in proofmarket.org, a market for proofs against money:
https://twitter.com/proofmarket/status/465206868403449856

Moreover, the fix looks trivial to backport to 2.3.2 (codewise). Two stables
releases (2.3.2.1 and 2.3.2.2) happened after that. A new bug report on the same
issue, specifically on the stable version, was closed because the bug is fixed
in the development version
(https://code.google.com/p/agda/issues/detail?id=1107#c1). To me, that's even
more problematic.

Now, maybe I'm asking too much, but I cannot trust Agda with serious proofs if
current releases have known soundness bugs for one year, even though they've
been fixed right away. I and my colleagues have used Agda for the paper I'm most
proud of, and we were aware of the risk of running into *UNKNOWN* soundness bugs
(that's unavoidable). Known trivial soundness bugs is another matter entirely.

Maintaining a stable branch where fixes can be backported right away, and/or not
closing bugs unless the fix is backported (or having separate backporting bugs),
makes such issues much harder. To me, not doing that systematically of that in
2014 is the software engineering equivalent of writing critical software in C -
no offense intended. (Not that I am a software engineering fan).

Instead, Agda has no stable branch. I've investigated the release process
leading to 2.3.2.1 (https://code.google.com/p/agda/issues/detail?id=864,
http://code.haskell.org/Agda/notes/releases), and I think it explains why such
problems seem hard to prevent with the current process. It seems somebody just
thought about which fixes to include, and forgot some. But the idea you can just
remember such things is a fallacy.

This quote from the release instructions is revealing:

(This would be unnecessary if we had two repositories, one stable and one for
development.)

Now, with git, it takes less time to backport a commit than to run the tests:

git checkout 2.3.2-branch
git cherry-pick $patch_hash
# handle conflicts if there are any (I expect none in this case)
git push
# At release time
git tag 2.3.2.1
git push --tags

With git, a single repo is enough for this, and can support an arbitrary number
of version branches. But I don't know whether you should switch to git; I just
think there must be a way to avoid this situation.

(The release procedure also look far too complicated and uses too little
automation, and it prevents releasing fixes right away, and the fact that
changes are only pushed at then end prevents somebody else from double-checking
the release before it's done).

For reference, below's what I could get from darcs about the fix, even though I
am positively unable to learn darcs. By inspecting the source, it seems the
patch applies directly to Agda 2.3.2.

$ darcs changes --match 'hash 20130506150241-5187b-
f673bbd081344a5bd40444550c7044d12cc95668' -v
Mon May  6 17:02:41 CEST 2013  Andreas Abel <andreas.abel at ifi.lmu.de>
  * Fixed issue 843: incorrect translation of let-bound patterns into
    projections.
    hunk ./src/full/Agda/TypeChecking/RecordPatterns.hs 73
    -    comb prj p = map (prj .) <$> recordPatternToProjections p
    +    comb prj p = map (\ f -> f . prj) <$> recordPatternToProjections p
    addfile ./test/succeed/Issue843.agda
    hunk ./test/succeed/Issue843.agda 1
[...]

$ darcs diff --patch 'hash 20130506150241-5187b-
f673bbd081344a5bd40444550c7044d12cc95668'

darcs failed: Text.Regex.Posix.String died: (ReturnCode 17,"illegal byte
sequence")

Cheers,
Paolo