Xiaokun Luan (Mar 13 2024 at 01:43): Xiaokun Luan (Mar 13 2024 at 01:43):Hi all,
I want to parse some Isabelle/ML files, is there any parser of Isabelle/ML? It seems that Isabelle/ML is a superset of Standard ML, and PolyML's parser cannot handle some features of Isabelle/ML.
Manuel Eberl (Mar 13 2024 at 10:53):This might be tricky due to the presence of antiquotations, which can run arbitrary ML code and depend on the Isabelle context in which they appear…
Mathias Fleury (Mar 13 2024 at 12:45):The real question is why you would want that parsing of SML…
Hanno Becker (May 02 2024 at 04:33):What exactly would you like to do? If it's about ML arguments (as in apply (tactic <{TACTIC>), where {TACTIC} is any ML expression of type tactic), one can do that
Xiaokun Luan (May 27 2024 at 07:27):Thanks for your replies, and sorry for my late reply.
I noticed that many ML functions are changed during the version update of Isabelle, and I want to develop a tool to auto diff the Isabelle/ML source code to generate a list of changed ML functions/values, such as renamed, moved, deleted, or changes in the signature. (Maybe this could be complementary to those breaking changes in the release notes?)
My current workaround is to write a simple parser using parser generator to handle part of the ML code. It can produce a summary of some breaking changes made to ML code, but I suppose that it can miss a lot of such changes because it cannot parse all ML code.
Mathias Fleury (May 27 2024 at 07:29):how do you define "breaking changes"? every rename is a breaking change if you are using the function
Mathias Fleury (May 27 2024 at 07:30):Otherwise I would suggest the very stupid git diff --word-diff -no-index isabelle2023 isabelle2024 to see what changed…
Xiaokun Luan (May 27 2024 at 10:07):Mathias Fleury said:
Otherwise I would suggest the very stupid
git diff --word-diff -no-index isabelle2023 isabelle2024to see what changed…
I think at least rename, move, deletion, and change of signatures should be considered as breaking changes. What I want is more like generating a summary from the diff results, just like those in the release notes, like Context.theory_name ~> Context.theory_base_name. Of course we can do this manually, but it is always good to have some automation, right?
Mathias Fleury (May 27 2024 at 15:57):the more complicated question: is it an oversight that it is not documented. Or is it on purpose, because you are not supposed to use it?
Xiaokun Luan (May 28 2024 at 05:48):I understand that most users don't need to use ML functions in their formalization and proofs, so it is reasonable to not to document these things.
However, based on my own experience and observation, there are some situations that dealing with Isabelle's ML functions is the only way we can take. I will provide two examples.
(1) There are more than 400 ML/sml files in AFP entries, thought maybe not all of them are using ML APIs, it is true that some people built their systems based on them, such as Proof_Strategy_Language, and Context.theory_name (what I mentioned before) is actually used by some of them.
(2) The Scala library scala-isabelle (https://github.com/dominique-unruh/scala-isabelle) relies on ML APIs. In fact, because the API "Mutex.mutex" now has to be referenced as "Thread.Mutex.mutex", it does not work on Isabelle2024. qrhl-tool relies on this library, and some AI-based theorem proving systems also rely on this library to interact with Isabelle.
I'm not asking to add these changes in any official documentation. I just want to have a little automation for myself to save some efforts. I'm still relatively new to ML, so if there are some better ways to do this, I'm all ears.
Last updated: Dec 21 2024 at 16:20 UTC