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
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
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
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."
This archive was generated by a fusion of
Pipermail (Mailman edition) and