Re: [isabelle] folding and linking in jEdit; curry/split
On Thu, 18 Feb 2016, Jasmin Blanchette wrote:
Without appropriate context, statements like "metis is first-order" or
"metis is higher-order" or "metis is buggy" are close to meaningless.
This having been said, I notice that nobody ever confused Nitpick and
its backend Kodkod. I'm grateful I didn't call the tool Isabelle/Kodkod.
Maybe that is because Kodkod is sufficiently unknown outside its Isabelle
context -- or maybe this just proves my ignorance about Kodkod.
The distinction of jEdit the text editor and Isabelle/jEdit the Prover IDE
is particularly important, because we need to do justice to both.
jEdit has its own profile as high-end text-editor, although its best of
time is probably over (after the founder left the project in 2006).
Thus it is particularly important to strengthen what is left of the jEdit
community, and not assimilate its name and declare it dead. It definitely
requires patience to get important changes through the jEdit tracker
system, but it usually works. It is better to have approx. 5 people still
maintaining jEdit on Sourceforge, instead of taking it over and doing it
by 1-2 people on the Isabelle side.
People who want to be lazy and use a short word, may call all Isabelle
tools just "Isabelle" and it will be usually right. So instead of "jEdit
checks a proof document", "Isabelle checks a proof document" will make
This archive was generated by a fusion of
Pipermail (Mailman edition) and