[isabelle-dev] NEWS

[Makarius]

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.


 	Makarius