Re: [isabelle] Name clashes in theory names

On Wed, 5 Feb 2014, Lawrence Paulson wrote:

The theory loader indeed doesn’t cope with this situation very well. The namespace for theory names is completely global. The only sure remedy for the moment is to avoid generic theory names, and Auxiliary is a perfect example.

"Auxiliary" is indeed a bad name, although a slight improvement over the "Aux" that was there before, which causes strange effects on Windows that are worth a long carnival session. (As everybody knows, "AUX", "COM", "PRN" are special, and neither case nor file extensions count here.)

Actual theory names are indeed global, but we have to cope with some odd feature add-ons for many years, which pretend that theories do have some qualification (via directory structure), although they don't. This mismatch causes many problems.

Mizar and Wikipedia are large projects that cope with a flat name space, but we are computer-scientists so structured names appear more natural. I am actually making concrete moves towards properly qualified theory names since 10 years, although that is often forgotten and sometimes hard to believe. (Many recent tools will break when the theory name space itself becomes qualified. Moreover we have more than one place to look: the theory loader for TTY or Proof General is different from batch build, and that is also different from interactive PIDE.)

I have now made one round of looking, if it is feasible to make more checks, without getting the theory name space really right. Some minor improvements might emerge for the coming release, but bigger steps
are still unclear.


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