Re: [isabelle] detaching sml mode from Prover IDE



On Sat, 30 Aug 2014, Gergely Buday wrote:

first of all, thanks for the developers for the sml mode.

Note that the "sml mode" is a full-scale IDE.

In the narrow sense, there is an "sml mode" in terms of jEdit, but that is just the token handler for syntax highlighting.


Would it be possible to detach the sml mode of the Prover IDE from
Isabelle? If one wants to develop in Standard ML, downloading the
whole Isabelle release is too much of a good thing.

Can you be more specific about the last sentence? The Isabelle distribution is not exactly small, but I never heard any complaints about it being too big. Rather, most people are glad that (almost) everything is there by default and works without further ado.

There are three main parameters: download time/space, unpacking time, disk space. Which one do you experience as a problem?


The Isabelle/SML IDE could be made a bit smaller than the default Isabelle release, but not so much. I guess that 50% size reduction would be the maximum, after considerable efforts.

Just for marketing reasons, a "big" IDE might be actually better, because this is what users see from other IDEs as well.

An actual benefit might be a way to bypass the bulky Isabelle/HOL build process, and just use Pure, but that requires again some more features to select "installation options" on startup.


	Makarius





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