Re: [isabelle] [Isabelle2019-RC1] Unhelpful error message (and possible regression)



On 06/05/2019 09:39, Dominique Unruh wrote:
> 
> 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.

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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.