*** General ***
* The old 'def' command has been discontinued (legacy since
Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
object-logic equality or equivalence.
This refers to Isabelle/acb0807ddb56.
This small reform may serve as an example of AFP maintenance. I've spent
many years to have the Prover IDE edit projects as a whole, and we are
now pretty close to that due to the reform of session-qualified theory
names. Full scalability is still somewhat lacking, though: It requires a
bit of thinking and planning which sessions to edit in which order. The
ML process can sometimes become overloaded and spend minutes on GC /
heap compaction. The JVM process is also quite easy to overload with
tons of PIDE markup; maybe there are even memory leaks.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
