Re: [isabelle] What naming will cause potential errors?
On Sat, 13 Apr 2013, Gottfried Barrow wrote:
It seems there were several overlapping threads there, but as to naming,
someone eventually sort of asked, "Can you please enforce naming rules
so that we don't end up with error prone code that goes undetected." And
you sort of said, "I don't want to enforce anything I don't have to
enforce." Consequently, that's why I'll stay paranoid for years to come.
I don't think you have to be paranoid, as long as you stay somewhere in
the middle ground what you normally see in public Isabelle applications.
Concerning enforcement of rules, there has been a slight tendency over the
years to become more strict: tell more explicitly via errors or warnings
instead of just writing manuals about the system. It is always a long and
tedious process to do so, since one first needs to pin down the rules
precisely, implement them, update existing applications accordingly, and
finally handle seasoned users who argue differently.
At this time, I'm not concerned with any errors that can result from
using external tools, only errors produced by the tools that Isabelle
officially supports. If the purple bar turns grey at the command "end"
in my THY file, and that represents that my naming conventions won't
cause problems with other Isabelle tools, then that's good enough for
It is hard to tell where "internal" ends and "external" starts. The
Isabelle/HOL code generator for Haskell is part of the standard Isabelle
disctibution, and used routinely in many applications.
Another example is the file-system: Is that internal or external to the
prover? A theory called "\<A>\<^isub>1" won't work for relatively obvious
reasons; one called "Aux" is less obvious -- it used to work in
Isabelle2012 due to Cygwin, but the Scala/JVM build system now insists in
Windows/MS-DOS conformity. Further uncertainty is introduced routinely
due to case-insensitive file-systems.
Note that Isabelle/jEdit has its own way to manage files for the prover,
so there are subtle differences to someone used to Proof General.
I imagine a scenario like this. Someone says, "I tried to use your
theory, but it's causing a ton of errors in another Isabelle tool, and
it's because of your naming scheme." And I reply, "I see. It's very
unfortunate that for these last 3 years I never had a need for that
tool, and I now regret again that my simplistic view of the world has
again caused me trouble."
This can always happen. Theory developments being used by others will
have to be refined and smoothened. A similar smoothening effect happens
to user applications after more than 3 updates of the underlying Isabelle
version -- I think you have noticed this already :-)
This archive was generated by a fusion of
Pipermail (Mailman edition) and