Re: [isabelle] Isabelle and Vim (was: Re: Another newbie proofs)

On 05/04/2019 14:08, Mathias Fleury wrote:
>> On 5. Apr 2019, at 13:45, Wolfgang Jeltsch <wolfgang-it at> wrote:
>> Am Freitag, den 05.04.2019, 12:21 +0200 schrieb Makarius:
>>> On 12/03/2019 17:15, Wolfgang Jeltsch wrote:
>>>> By the way, have there been any attempts so far to integrate
>>>> Isabelle into Vim?
>>> No, Isabelle is moving in the opposite direction.
>> In what respect is Isabelle moving away from Vim?
> Away from these old single-threaded text editor towards the glorious Prover-IDE infrastructure.

Yes, when I started the Isabelle Prover IDE project around 2008, I made
jokes about Eclipse as "16 tons on your desktop" (as in Monty Python).
Now we have a much better platform than Eclipse (Isabelle/jEdit version
11), but it is "32 tons on your desktop".

I did not plan for that weight and gravity, but it is a natural
consequence of a "filthy rich client approach" of IDEs.

Just a few weeks ago, I updated my home machine again after 5 years. For
just 1650 EUR I got:

  * 8 CPU cores at 3600 MHz sustained clock frequency without fan noise
(or 4900 MHz with a lot of fan noise)
  * 32 GB RAM at 3600 MHz (instead of normal 2666)
  * 1000 GB non-volatile RAM (PCIe) for the file-system (not "disk")

Thus the richness of Isabelle can be enjoyed without feeling the weight.

Note that Isabelle has always required serious equipment. I remember
when Proof General 2.0 with XEmacs 21.1 was the great new thing in 1999,
it required hardware for 12000 EUR on the desk, or a big server
somewhere in the back.


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