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



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.






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