Email Gateway (Aug 23 2022 at 08:53): Email Gateway (Aug 23 2022 at 08:53):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,
I am still a relatively new user of Isabelle and this is the first time I
am going through the process of adapting any remotely serious previous work
to the new release. I have a question with regard to how the changes are
documented in the NEWS.
Do all undocumented (in the NEWS) changes in the Isabelle/ML infrastructure
correspond exclusively either to the
- improvement of the efficiency
- changes to the structure and naming conventions of the public interface
- introduction of the new functionality/features
- withdrawal of components from the public interface
?
Background
I noticed that there has been a substantial number of changes to the
Isabelle/ML infrastructure between Isabelle2019 and Isabelle2020 release
candidates. I would like to understand whether or not there is any
criterion for when a change needs to be documented in the NEWS and when it
does not need to be documented. In my previous post (
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2020-April/msg00027.html)
I commented on a NEWS entry that was concerned with a change in one
particular Isabelle/ML function. However, having analyzed changes more
thoroughly, I realized that this entry was concerned only with one out of a
substantial number of Isabelle/ML functions that were moved and/or renamed
and/or changed in some other way. However, none of these changes seem to
have been documented in the NEWS.
Some examples of such seemingly undocumented (in the NEWS) changes include:
- Facts.name_of_ref => Facts.ref_name
- Thm.name_derivation: string -> thm -> thm => Thm.name_derivation:
string * Position.T -> thm -> thm
- Drule.RNS => Basic_Thm.RSN
- ...
Of course, in most cases, it is sufficiently easy to trace these changes
and adapt your own work to them. My primary concern is how much should one
rely on the NEWS when adapting to the changes? For example, is it
anticipated that if I rely on an invariant established based on the
analysis of the implementation of an Isabelle/ML function (e.g. thm->thm)
in Isabelle2019, then this invariant will still hold in Isabelle2020,
provided that my analysis is correct and nothing is mentioned about this
function in the NEWS?
Kind Regards,
Mikhail Chekhov
Email Gateway (Aug 23 2022 at 08:53):From: Makarius <makarius@sketis.net>
The NEWS file says "history of user-relevant changes". Things that are missing
are either not relevant to general users of Isabelle/ML or somehow irrelevant
(trivial).
A change in the signature (without change of meaning) is rarely documented:
the ML compiler will tell you about the change and you can make it happy on
the spot, e.g. Thm.name_derivation above.
A change in the semantics will never happen without a change in the signature.
Usually it will get a new name, and if relevant a notice in NEWS.
Sometimes changes rolling over your applications merely indicate odd uses of
internal names. E.g. Basic_Thm.RSN is nothing you would ever write in user
space. The standard name is just "RSN" (infix) or "op RSN" (prefix) and that
did not change.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC