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 proper sense.


	Makarius




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