Re: [isabelle] Comparing Isabelle/Scala with scala-isabelle. Was: Isabelle code for getting in-memory representation (abstract syntax trees) for complete theory file (tree of loaded theories)
- To: Dominique Unruh <unruh at ut.ee>, Wenda Li <wl302 at cam.ac.uk>, Alex Meyer <alex153 at outlook.lv>
- Subject: Re: [isabelle] Comparing Isabelle/Scala with scala-isabelle. Was: Isabelle code for getting in-memory representation (abstract syntax trees) for complete theory file (tree of loaded theories)
- From: Makarius <makarius at sketis.net>
- Date: Thu, 11 Feb 2021 14:22:15 +0100
- Authentication-results: mx2f26; spf=pass (sender IP is 62.216.204.123) smtp.mailfrom=makarius at sketis.net smtp.helo=[192.168.178.32]
- Autocrypt: addr=makarius at sketis.net; prefer-encrypt=mutual; keydata= mQINBFcrF+4BEADMcXMnu3XHg6bRsGe3tajAHqvm89+ecn/Y0WhjI2FplhkZs1LwM+ZA9eXh hiBrC/yX0FJ+qjzVIfm66CX4nzVG1f8qwaervMpvpA+gbhtQiXc0t+LDcqV+5cdtpKplPHSu oW+KzJKyCdkDB5fYMOzuaXQwYi12YAEQH2r6K7Q7Np+k82Xli1pWe+Tha/BH0pKJ5Q01aPep ASrNW9F+moX7C0fxWl65LiXGmF0UJep6fqKruhy8oNF4p6I2oZhktvaR/x6tkL2PkT3r+xUS 6g5i3BOjfwhoGY57nsioeK+8VFvdRH5DK4CbrTgDl7ddcrEeENrfpDiPLs/afVbe/T9oDXmJ OJAO4WMpfZNiFhx9SSVTHohw29Fyzn0N1UQGjPqAY1jg32DAxlnMQ0co/KabEFAcoQsW1/6U ZGiNxYVIyEKGrnSY4WuLuNC8CmU1RaYSdTk1y9tYdxufM9lH9ynzJwac6FdalOOxMR2G9JG8 L9/dk3ytlP6DVwkPBSCpJaTkTyMp1wSkF1oK/BDu5xKUQh0zvvLCuZ16hiKRBBSjpVExXRZC u+NC1Y4wqm1HOH7HBwgZ1Hv9S/EPmI9iwgcW0SpDJqPf2Cm7oFMZsZ5Dbs6/nOQoe4Zegy45 ymqDRlIekP7zj+vOoR80XAYfmAH5DElJHldcjmgLBMdpvvqGZwARAQABtB5NYWthcml1cyA8 bWFrYXJpdXNAc2tldGlzLm5ldD6JAj0EEwEIACcFAlcrF+4CGyMFCQlmAYAFCwkIBwIGFQgJ CgsCBBYCAwECHgECF4AACgkQ89KUEoG/TbiVrw/9FjEBgh2CB7Qof7Y4k0yc7j+x/A0Wmkc0 iwP5jaKJuxRv1JJT8CFqm392+/cdh3EkRUk/UWD+hpNndYJwxZltrEpKVqFAWoVOg3ZJ4cuI MYhlp4tk/T0KSl/gKT16dc6uJ7M/FzW0zv50vjFtAdianEDuqLXHKaGDUwWoOTDly0gdZ7aH /eNby6ONHUSJMdTNOErh2N+uESM4aZqUuuL/dTb6xiVzCpV5saT8EMakoazUd7QhoBaHvqfs BL7DEmvcTtA79GF3ufHrF/UndIcx8aMznZ2PGNjmy5seDCoKX0EYHdLam8vgo/TuU4dRw5Zn 6E/ouyNOliXT1Mn+SomeBSXTR5MXRq4TQ9MKVGiP0Yl+7GJQU0JFtDC1ZZEOyjIiwGWOhbUR pYujVm8C1iQ7NcEn2BqOAmRML6IR6+En4RLbgCNsBNXlmTPRJOaI+iV6DZzg3x9zcaDGhoYt jkBTEFpb0F3jU9yuaEU5401NV34fUxg8tqXs0R9CKinO7kQ8N+RDjyyY8k2KZiDYBJ6r+OK0 d7TaTj7F9tmpAu2pmQ8lxOKjDZIwlbGTsC4lxISmcPzBGTKXja5nakcWYx/lZ4vje0WZ12HN amnD1weakFixRYit0d+Kz7cuj684NSbhwC0oN2t9R06Nfq8UPEWRKEitCly0OtRgio8zVZ/L eAC5Ag0EVysX7gEQAKs5NVOvYkE/r8KLsJ8/L/9eulpJDOFilZ9fyuqii7t1UpHZLb58QghW JM+IB2GSGsB+pOi6Je7hmwxcVdXYbGlYZ4Btqqw48/XptfbNZ8alCk6AqoVFP4MbYxij/Qqv f/Yw6GR0p1RIC/W4GF/JgDDwDFEiMT6Pv6dpM8acdNFCERDZdoOJiC+XJRwy5lZ2g5FOJkT9 rVI9EnA7mBXLLjPOMUp2/eZxN6gKOZzI3ej9vixg3adWR2yfKPgacHP/ujnVfITOl0OyLE5f zIHq85dEV4zW6Mpx7+Um0tdkwlUVMaW2nQ1bcwejgVAuD/MLSF/lSs3N5D1ctw5QUemYh7/e 2dC12UJuFDFxNPzcltQTlkBCVWV1D0SjScDHdlF6HhzpZOlt52/rwTn5GHtY4nwAL4IJ+Yvl WX8YKmyILH4Ai8c/N2IVRERQ2qorWFlsQnqrXV+hXf8aUwjc/pq4K9rsWxvle3TpeZfoBefU /s1PEX0SepZFAqAXHlQ9DZPsdPDo9EFK695G5w4nf03EhE9TV1MKGUuc1XJ6f1ZLaxu0TwTA 6qYtKIyBcU0Yn61S2Kh7Dgb5LdLV8nfl71+n/xIt2IWH5UJ9YuwEgGEP0c6ImnAUZ+nRodFI 0RwtCWlRkSJWtQln1vcphrz8PjWZH6e/nWnceXR/Al5P0WexQgtvABEBAAGJAiUEGAEIAA8F AlcrF+4CGwwFCQlmAYAACgkQ89KUEoG/Tbh7VQ/9Fc4bdwJYc3jH/LiuXv6uMg50Cv6lg2NT bL9DClWGNiYzejfM2A4c5K+GRUXhyD7S9U203MOv3z7uTbtyQL8XVolNnQlRIkB00f8nJ2sw HMXx/hemjXBvtlneq+vrMORJexldXUMFq19ZZrvj0zZL+pUnGFqt+IWTEE5GpL7wu20Demaj jYyGyKcDZyJOWZcl4e45Yn3hl0EI2xVmVh7ZinVsb3+nqgcltFy4Jt+drezwV2EiLGJHfGsT jEQb3C9VpneU4Jo+hHtfqLK4Q8+WlIOzSfyvwbabxrhyqg7i11fu8yckNW3dCURPYigV07HK 4dN0zhj53M0Q3eTwegJRPJb8XoLDcSdbsaU2HIShlGDKmzS9KL4JzLikQ9dXROC4cae3jRKH aexFi4B55Ab6FxIfXj09wUCO6Nm0owDfIBDMgiywvi2Rb2etCjBgRbSj71S2nntd9ZitoYvE yKirLkWmJRbp3ln8cHi8Uc/jr1cDPVRWuLUN0uceMj5+AR+NZVakcNUHWJCinMMjacho0SyP QmocdU8pzzupreaVWruqaSzqcpWBPwrE5OxEtJ+OyIBjKmRJ5eptjh4rKgNaVnKjhqbvr+Yz pUAgPp38jjf4HJghUGIfWArKNelKJEJOYk94DAbmT67LgqEdZ0yaA2BCHmreN727WIzV9vkX NMc=
- Cc: Isabelle Users <isabelle-users at cl.cam.ac.uk>
- In-reply-to: <d1a71369-5823-0064-bed3-97f5196df809@ut.ee>
- References: <DBAP191MB12917F27E19CA304587A6A3B80B89@DBAP191MB1291.EURP191.PROD.OUTLOOK.COM> <BEBFE0A8-03B9-4C84-BF1E-E6B87215703D@cam.ac.uk> <85f2e96f-b158-356f-de59-d1123e23dfd7@sketis.net> <ac937108-8084-cf3c-1752-7c70d460a301@ut.ee> <75e54c48-4e5a-a373-b0e4-fb6db558fb2d@sketis.net> <d1a71369-5823-0064-bed3-97f5196df809@ut.ee>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.10.0
On 11/02/2021 12:53, Dominique Unruh wrote:
>
>> Exactly. Over 10 years I have given many talks and written many papers about
>> Isabelle/Scala in contrast to Isabelle/ML. The main idea:
>>
>> * Isabelle/Scala is for systems-programming / system integration
>>
>> * Isabelle/ML is for mathematical logic
>>
>> Sometimes there is a bit of overlap, and some freedom to decide where things
>> happen. But when you start to do term operations in Isabelle/Scala it is
>> probably wrong.
>
> Good. Then I got things right. So we have a clear separation of purposes
> between Isabelle/Scala and scala-isabelle.
>
> *
>
> Isabelle/Scala is for systems-programming / system integration
>
> *
>
> Isabelle/ML is for mathematical logic
>
> * scala-isabelle is also for mathematical logic (and for any other more
> low-level inspection of Isabelle data)
>
> Anythings that can be done in scala-isabelle can also be done in Isabelle/ML,
> of course. (And vice versa.) However, if due to the constraints of the
> project, we want to use Scala (or any other JVM language), then scala-isabelle
> would be the right choice.
The choice is up to you. Within the regular Isabelle ecosystem, the proper
language for heavy-duty symbolic logic is Isabelle/ML: it has been made
precisely for that over 35 years. We could not crunch the great things in AFP
without Isabelle/ML as it is today.
To conclude this overview of possibilities, here is a further NEWS entry from
Isabelle2021:
*** ML ***
* Antiquotations @{scala_function}, @{scala}, @{scala_thread} refer to
registered Isabelle/Scala functions (of type String => String):
invocation works via the PIDE protocol.
This means that Isabelle/ML programs can appeal to operations in Scala, if
that happens to be available on that side, e.g. for historical reaans or
existing Java implementations. Thus the order of control is straight-forward:
ML hands over to Scala like a regular function call, without any special
programming tricks exposed outside.
An example application is Nitpick/Kodkod, which works either as a heavy JVM
process or light Scala thread (both invoked from Isabelle/ML):
https://isabelle.sketis.net/repos/isabelle-release/file/Isabelle2021-RC5/src/HOL/Tools/Nitpick/kodkod.ML#l1003
https://isabelle.sketis.net/repos/isabelle-release/file/Isabelle2021-RC5/src/HOL/Tools/Nitpick/kodkod.scala
Side-remark: Originally I wanted to get rid of the JVM process for
Isabelle2021, but this has to wait for the next release, due to remaining
assumptions in the Kodkod implementation concerning the Java context
(interrupts, threads, exit).
> Scala is easier to debug and edit with
> modern IDEs. Isabelle/ML has some support
> (e.g., ctrl-click is useful), but imho it
> does not come close to the tool support
> that we have in modern IDEs.
The term "modern" sounds very old-fashioned to me. Modern times have ended
some decades ago; we now have the post-modern era.
For Isabelle projects, the Isabelle Prover IDE has very good integration of
everything: Isar, ML, other sub-languages. I know this best and like this
best. It is also quite easy to integrate your own sub-languages with PIDE
support (implemented all in Isabelle/ML).
Isabelle/Scala is an exception: it is not (yet?) integrated into
Isabelle/PIDE, but the "isabelle scala_project" tool allows to generate a
Gradle project for use in IntelliJ IDEA: I do like that IDE, but that alone
would never be a reason to disregard our fine Isabelle/ML working environment.
VSCode is another popular quasi-IDE option: Isabelle/VSCode is a minimal
experiment, much more could be done. Generally, I see a lot of IDE concepts
retrofitted into the VSCode editor project, but it might require 5-10 more
years to become a proper IDE.
Makarius
This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.