Email Gateway (Aug 22 2022 at 14:52): Email Gateway (Aug 22 2022 at 14:52):From: Nemouchi Yakoub <y.nemouchi@gmail.com>
Dear All,
In Isabelle 2016 the structure Thy_Load does not exist (at least for
Windows distribution).
The function Thy_Load.master_directory is renamed
Resources.master_directory
No of these changes are mentioned in the NEWS.
And imao this line: "ThyLoad ~> Thy_Load" in the NEWS file is useless the
structure does not even exist. Again I am talking about Windows
distribution unless there is some command to execute in order to include
this structure in the build!!
Best,
Yakoub.
Email Gateway (Aug 22 2022 at 14:53):From: Makarius <makarius@sketis.net>
On 15/12/16 22:16, Nemouchi Yakoub wrote:
In Isabelle 2016 the structure Thy_Load does not exist (at least for
Windows distribution).The function Thy_Load.master_directory is renamed
Resources.master_directoryNo of these changes are mentioned in the NEWS.
Do you mean Isabelle2016 (February 2016) or the current Isabelle2016-1
(December 2016)? Anyway, the renaming of structure Thy_Load to Resources
happened between Isabelle2013-2 (December 2013) and Isabelle2014 (August
2014):
http://isabelle.in.tum.de/repos/isabelle/rev/06cc31dff138
The NEWS file covers only "history of user-relevant changes", while the
true history is managed by Mercurial. Both need to be consulted
occasionally.
Not every small change ends up in NEWS: the above could have been added
or not, depending on an estimate how user-relevant it really is. The
master_directory has actually become a bit less relevant to Isabelle/ML
user codes, because Resources.parse_files and
Resources.provide_parse_files have taken over the details of managing
external sources in a way that also works with the Prover IDE (but that
important change is not document either -- it needs to be derived from
the typical uses in the sources).
And imao this line: "ThyLoad ~> Thy_Load" in the NEWS file is useless the
structure does not even exist.
NEWS contains the cumulative (immutable) history of user-relevant
changes. The renaming of "ThyLoad ~> Thy_Load" belongs to Isabelle2009-2
(June 2010). This can be seen in the SideKick tree view of
Isabelle/jEdit -- the NEWS file says in the very beginning:
Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.
I find it very hard to work without the Prover IDE these days. It is
relevant for the NEWS file, ROOT files, ML files, thy files ...
Makarius
Email Gateway (Aug 22 2022 at 14:53):From: Nemouchi Yakoub <y.nemouchi@gmail.com>
I got your idea Makarius and you explained me that before.
My point by saying the line "ThyLoad ~> Thy_Load" is useless was to mention
that:
If a given change on a function or a module was relevant why at some point
changes happen on the same thing with the assumption that it is not
relevant anymore.
Email Gateway (Aug 22 2022 at 14:53):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Yakoub,
I believe I can answer that one:
Isabelle is developed by many people over many (30) years. Asking us to be 100% consistent in terms of determining what is relevant for the NEWS file is asking too much of mere human beings.
As a general rule, you can assume that the vast majority of changes to the ML interface are not going to be documented (beyond the Mercurial history). This is unfortunate, but documenting every change would put a too heavy burden on the developers, given the ratio "users of ML interface : developers". For a project with 10, 100, or 1000 users (and, hopefully, more developers and higher salaries for them and no requirement to publish or perish), the situation would be different.
Cheers,
Jasmin
Last updated: Apr 25 2024 at 12:23 UTC