Email Gateway (Aug 22 2022 at 19:43): Email Gateway (Aug 22 2022 at 19:43):From: Makarius <makarius@sketis.net>
There is a deeper problem behind it: Isabelle2017 and Isabelle2018 were
a bit too liberal in the reform of session-qualified theory names, still
admitting odd sub-directory layouts and shared sub-directories for
different sessions.
For Isabelle2019, I had some plans to clear this out: allowing theory
sources to reside only in explicitly specified session directories. Thus
most of the uncertainty of theory file location would go away. I did not
manage to re-open this on time, so it is postponed to a later release.
So the overall situation in Isabelle2019 should be mostly the same as in
Isabelle2018.
Makarius
Email Gateway (Aug 22 2022 at 19:47):From: Dominique Unruh <unruh@ut.ee>
Hi,
I updated to 2019-RC1 but forgot to update afp-devel to the required
version (it was still on af53c1f41e1c). When starting jEdit, I get the
following message (as a popup):
/opt/Isabelle2019-RC1/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar:
Cannot start:
*** Duplicate theory
"/opt/Isabelle2019-RC1/src/HOL/Library/Countable_Set_Type.thy" vs.
"HOL-Library.Countable_Set_Type"
The problem is solved by updating AFP. However, I wonder whether this
error message can be improved, e.g., by indicating from where the
duplicate theories are included (this might be beyond the scope of the
RC, of course, if the information is not already available at the
location where the error is generated). Otherwise figuring out where the
error is may involve a lot of detective work and try and error to narrow
down where the problem comes from.
Secondly, I wonder whether this message indicates a regression. If I
remember correctly, in 2018(?) a mechanism was introduced that allows
Isabelle to recognize when the same theory file is loaded via two
different paths. (I may misremember.) The present case looks like an
example of this. So should this error even occur?
Best wishes,
Dominique.
Last updated: Apr 18 2024 at 01:05 UTC