Stream: General

Topic: Workaround for duplicate theory name clash?

view this post on Zulip Christian Pardillo Laursen (May 08 2024 at 15:48):

Hi, I'm trying to import a theory from the AFP which has a name clash with another of my theories.

theory Martingale_Compat
  imports "Martingales.Martingale" Stochastic_Process

gives error

exception THEORY raised (line 359 of "context.ML"):
  Duplicate theory name
  {..., HOL-Probability.Essential_Supremum, HOL-Probability.Stopping_Time, HOL-Probability.Probability, Draft.Dyadic_Interval, Stochastic_Process}
  {..., HOL-Probability.Infinite_Product_Measure, Martingales.Filtered_Measure, Martingales.Measure_Space_Supplement, HOL-Probability.Independent_Family, Stochastic_Process}

Is there any workaround for this? Stochastic_Process is a pretty canonical name for my theory, I'd rather not change it if I don't have to.

view this post on Zulip Mathias Fleury (May 08 2024 at 15:50):

Sadly no, there is no work-around. You really have to change the name.

view this post on Zulip Mathias Fleury (May 08 2024 at 15:52):

That is why there is a Multiset_More and a Multiset_Extra in the AFP (and a Multiset_More2 I have seen it somewhere)

view this post on Zulip Manuel Eberl (Sep 15 2024 at 10:26):

Isabelle is an old system and much of its architecture comes from a time when no one envisioned proof developments with more than a few theories.

This particular issue has been on Makarius' to do list for a very long time, but many things need to happen before it will actually work. It will probably happen eventually, but until then, renaming is the only workaround.

Last updated: Dec 21 2024 at 12:33 UTC