Email Gateway (Aug 19 2022 at 13:44): Email Gateway (Aug 19 2022 at 13:44):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear all,
we just spent one hour to detect why a singleton entry in the AFP compiled successfully,
whereas just adding this entry within a larger development resulted in an error.
The problem would have been easy to detect, provided there would have been any warning message
that there are two theories called "Auxiliary" where silently only the one theory is kept.
However, starting isabelle build -v ... just complained about some unknown facts, which at least
to us did not at all point to real error of the name clash.
(We imported none of the "Auxiliary"-theories directly)
In order to ease such debugging in the future, we would appreciate any integration of warning messages
in the case of name clashes of theories.
Kind regards,
Chris and René
Email Gateway (Aug 19 2022 at 13:44):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Seconded. I also ran into this problem a few times.
Andreas
Email Gateway (Aug 19 2022 at 13:44):From: Lawrence Paulson <lp15@cam.ac.uk>
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.
Larry Paulson
Email Gateway (Aug 19 2022 at 13:44):From: Peter Lammich <lammich@in.tum.de>
Seconded. I also ran into this problem a few times.
Me too.
For me, its an indication that Isabelle's simple name-space model is not
adequate for programming in the large, but it is exactly that what we do
in some of our developments, depending on >10 AFP-entries.
Email Gateway (Aug 19 2022 at 13:44):From: René Thiemann <rene.thiemann@uibk.ac.at>
Seconded. I also ran into this problem a few times.
Me too.
Thanks for your agreements.
For me, its an indication that Isabelle's simple name-space model is not
adequate for programming in the large, but it is exactly that what we do
in some of our developments, depending on >10 AFP-entries.
Indeed, a more structured name-space model would of course be most welcome,
but I imagine this would be a larger effort than just a adding a warning message.
Kind regards,
René
PS: We are currently depending on 14 AFP-entries.
Email Gateway (Aug 19 2022 at 13:50):From: Makarius <makarius@sketis.net>
"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.
Makarius
Last updated: Apr 25 2024 at 20:15 UTC