Email Gateway (Aug 19 2022 at 15:41): Email Gateway (Aug 19 2022 at 15:41):From: Gergely Buday <gbuday@gmail.com>
Hi,
first of all, thanks for the developers for the sml mode.
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.
Would this detachment make sense from the Isabelle maintainer's viewpoint?
How much effort do you see for this to be done?
Email Gateway (Aug 19 2022 at 15:52):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 19 2022 at 16:02):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Gergely,
since the SML mode is implemented using the infrastructure of
Isabelle/ML and PIDE itself, there is no economic way to do so. Of
course you can e.g. strip all the object logic sessions (HOL, FOL, ZF),
but this has no dramatic impact.
Florian
signature.asc
Last updated: Oct 30 2025 at 08:28 UTC