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 me.

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 :-)


	Makarius




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