Re: [isabelle] Isabelle and Vim (was: Re: Another newbie question...case-based proofs)



On 05/04/2019 14:08, Mathias Fleury wrote:
> 
>> On 5. Apr 2019, at 13:45, Wolfgang Jeltsch <wolfgang-it at jeltsch.info> 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.


	Makarius




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