search

dominique-unruh / scala-isabelle

A Scala library for controlling/interacting with Isabelle
https://dominique-unruh.github.io/scala-isabelle
MIT License
37 stars 7 forks source link

Support for Isabelle2024 #14

Closed BookWood7th closed 4 months ago

BookWood7th commented 5 months ago

The internal ML structures of Isabelle have changed in the last Isabelle update. This makes scala-isabelle not work for the new Isabelle version.

Is an update to scala-isabelle planned to ensure compatibility with the new Isabelle version?

marcinwrochna commented 5 months ago

Fortunately there's only two changes that seem to matter: A. Mutex is now Thread.Mutex B. Isabelle/ML explicitly rejects 'handle' with catch-all patterns. INCOMPATIBILITY, better use \<^try>‹...› with 'catch' or 'finally', or as last resort declare [[ML_catch_all]] within the theory context. (citing the release notes).

I have a branch that works with Isabelle2024 by fixing A. and doing the ML_catch_all workaround for B., but:

  1. It's not backward compatible (I didn't add version checks).
  2. It would be better to replace the catch-alls with try-catch-finally in Scala_Isabelle_Master_Control_Program.thy instead of the workaround.
  3. I auto-removed trailing spaces which makes the commit diffs messy.

Unfortunately I personally don't have the time to make a proper merge request currently.

dominique-unruh commented 5 months ago

I will deal with this in the next few days. (I did it for one of the RCs and then forgot to finish it up when 2024 came out.)

dominique-unruh commented 4 months ago

ee5158b72d87dbdcc97ad800f9f5ed36bd6d320e supports Isabelle2024. A release is in preparation.

marcinwrochna commented 4 months ago

Thanks a lot!

dominique-unruh commented 4 months ago

Isabelle2024 support is now in release 0.4.3-RC1.