makarius at sketis.net
Thu Jan 5 20:42:05 CET 2012
On Thu, 5 Jan 2012, Lawrence Paulson wrote:
> I think your point is that somebody who spent a lot of effort making
> their code work with a development snapshot could be wasting their time,
> because the next release could be as different and require everything to
> be converted again.
Yes, but without the two occurrences of "could" above. A development
snapshot is hardly ever compatible with a proper release. Half porting is
double effort, and leaves a bad impression to genuine users who want to
use the system, not tinker with snapshots.
> I still think there is no harm using the mailing list to advise users
> that sets are going to change back to their former behaviour. At the
> very least, we can advise users to avoid using mem_def and confine
> themselves to the set primitives.
I don't understand the purpose of this. Incompatibilities for new Isabelle
releases are routine, so this would be not very informative.
I've started this thread merely to point out that the NEWS should tell
more explicitly how to do the porting, and avoid the known pitfalls.
More information about the isabelle-dev