Skip to content

Fix field names in Isabelle translation#3795

Merged
unp1 merged 2 commits intomainfrom
fixIsabelleTranslation
Mar 31, 2026
Merged

Fix field names in Isabelle translation#3795
unp1 merged 2 commits intomainfrom
fixIsabelleTranslation

Conversation

@unp1
Copy link
Copy Markdown
Member

@unp1 unp1 commented Mar 31, 2026

Updates the Isabelle translation to the new field name and observer symbol name conventions

Intended Change

The Isabelle translation should be able to recognize fields and observer symbols

Type of pull request

  • Bug fix (non-breaking change which fixes an issue)

Ensuring quality

  • I have tested the feature as follows: automatic tests should run through again

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

@unp1 unp1 added the 🐞 Bug label Mar 31, 2026
@unp1 unp1 added this to the v3.0.0 milestone Mar 31, 2026
@unp1 unp1 requested a review from WolframPfeifer March 31, 2026 11:31
@unp1
Copy link
Copy Markdown
Member Author

unp1 commented Mar 31, 2026

The failing test is just because of maven not being able to access the javaparser repo.

@unp1 unp1 force-pushed the fixIsabelleTranslation branch from 429f91c to 41e52dd Compare March 31, 2026 11:43
Copy link
Copy Markdown
Member

@WolframPfeifer WolframPfeifer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! I didn't remember that we should have adapted this after changing the name prefixes for fields. I think, we don't have any test for the Isabelle translation at the moment (because that would require running Isabelle), right?

Maybe it is a good idea to use Patter.quote() instead of the manual escaping with backslashes? However, I approved the PR and leave that decision to you.

@WolframPfeifer WolframPfeifer added the keyext.isabelletranslation Module: keyext.isabelletranslation label Mar 31, 2026
@unp1 unp1 force-pushed the fixIsabelleTranslation branch from 3c89bc5 to 7ec539f Compare March 31, 2026 12:00
@unp1
Copy link
Copy Markdown
Member Author

unp1 commented Mar 31, 2026

Thanks! I didn't remember that we should have adapted this after changing the name prefixes for fields. I think, we don't have any test for the Isabelle translation at the moment (because that would require running Isabelle), right?

As far as I know we do not have some.

Maybe it is a good idea to use Patter.quote() instead of the manual escaping with backslashes? However, I approved the PR and leave that decision to you.

Thanks! It makes now use of Pattern.quote(). I did not know about that one.

@unp1 unp1 enabled auto-merge March 31, 2026 12:04
@unp1 unp1 added this pull request to the merge queue Mar 31, 2026
Merged via the queue into main with commit 88c07fb Mar 31, 2026
32 checks passed
@unp1 unp1 deleted the fixIsabelleTranslation branch March 31, 2026 14:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

keyext.isabelletranslation Module: keyext.isabelletranslation 🐞 Bug

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants