Re: [isabelle] What naming will cause potential errors?



On 4/12/2013 3:38 PM, Makarius wrote:
There is nothing you "have to" follow. Naming conventions are a matter to keep things simple at very little cost -- they belong to "best practices".

Thanks for the lengthy reply. I'll take your word that I can name identifiers in any way that the prover engine will accept when I'm working in jEdit. Still, I'll remain paranoid about this for years to come.


Observing certain customs routinely saves a lot of energy to rethink and reconsider things over and over again. Sometimes this has to be done, nonethrless: e.g. for Isabelle/Scala I've re-used many Isabelle/ML conventions at the cost of violating other conventions on the Java Virtual Machine, and Scala itself tends towards very mixed ways of writing. I had to spend extra time to study history, manuals, websites to ensure that no bad consequences are coming from Graph.is_minimal in both Isabelle/ML and Isabelle/Scala, and not Graph.is_minimal here and Graph.isMinimal there (IAmNotGoingIntoDetailsWhyCamelCaseIsNotUsedInOurTradition).


Anyway, the mail thread you mention was initiated by the surprise that using a lower-case theory name in Isabelle/HOL makes the Haskell code generator fail due to resulting lower-case module name, which Haskell rejects.

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.

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.


You do get overlaps in certain more complex cases nonetheless, but the convention is somewhat better off than doing it just arbitrarily.


I've put some effort into coming with a naming scheme, mainly for the purposes of readability, name meaning, and consistency of style. My question here has been to try and not get vested in some naming scheme that comes back to haunt me.

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

Regards,
GB




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