Proof Scripts in JML#3657
Conversation
|
I have written an integer split command. An induction command is on the way with support for int, user-data types, bsum(?). Commit: 4644331 |
|
The history of this PR was totally changed while I was working on it. |
mattulbrich
force-pushed
the
jmlScripts
branch
2 times, most recently
from
96a6a98 to
2382655
Compare
mattulbrich
force-pushed
the
jmlScripts
branch
4 times, most recently
from
2066973 to
ae8b141
Compare
mattulbrich
force-pushed
the
jmlScripts
branch
from
07792f4 to
2bc3a36
Compare
mattulbrich
force-pushed
the
jmlScripts
branch
from
d5d10bf to
46567da
Compare
|
@WolframPfeifer Could you please revert the merge of main into this PR (and do a rebase instead, or just let to @mattulbrich for the sake of confusion avoidance)? This was a merge-free PR, which results in an easier-to-read git history. |
WolframPfeifer
force-pushed
the
jmlScripts
branch
from
ff1ce97 to
ec5929d
Compare
Ok, I reverted the merge. I see the point about a clean history. However, I am not sure what a good workflow would be. Should we do a merge with main only at the end of the feature development, before the merge of the PR? |
|
Thanks for investigating, Richard @unp1
Who is C? Or is it Claude? This branch is on a reduced github workflow. It seems that the parameters are parsed identically. (see details below). In the current version, all What definitely is different is the order in which the files are investigated. I added a sort routine to make this order deterministic. However, for some reason there are now again 8 merge conflicts even though I merged only last week; that is why the tests do not run. I do not know if I will find the time to do this merge in the next days. :( Grep results showing that parameters are identically parsed.AutoOnly2 fails on Windows, not on ubuntu. |
# Conflicts: # key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java # key.core/src/main/java/de/uka/ilkd/key/scripts/ProofScriptEngine.java # key.ncore/src/main/antlr/KeYCommonParser.g4
# Conflicts: # key.core/src/main/java/de/uka/ilkd/key/scripts/ProofScriptEngine.java
If you want I can try to get Claude doing the resolution and we both check afterwards that everything is correct? |
|
If C could do the merge and you review it, that would be splendid. My bet and hope is that c0a7ae8 will solve the problem. .. |
I do have a Windows machine: And it goes through there 🫢 . But not on the CI machine. Therefore, I assume the indeterministic file order may be the problem. This of course raises another issue: Why does this order matter? At least on could investigate then. ... if that is the reason. |
Resolve conflicts from the source-location move to key.ncore (KeYProject#3870): Position/Location now live in org.key_project.util.parsing. Updated the stale imports (JP2KeYConverter, KeyAst, ScriptCommandAst, JmlFacade, JMLTransformer, ApplyScriptsMacro) and moved the branch's Location.fromPositionInfo helper into key.core's JavaSourceLocations (it uses PositionInfo, so it cannot live in the now JavaParser-free ncore Location).
…ripts
The character loop's `case '\r' -> { }` did nothing, so a carriage return fell
through to the `cmdBuilder.append(...)` below and ended up inside the command --
e.g. in a quoted value that spans a CRLF line break. Script files are marked
`text` in .gitattributes and are therefore checked out with CRLF on Windows (and
depending on the CI runner's eol config), so scripts parsed there carried stray
'\r's and could fail to match. Skip the carriage return with `continue`.
Regression test (ScriptLineParser-level) added in ProofScriptParserTest; it fails
without the fix and passes with it.
Created with AI tooling
Windows != Windows. On Github, it is a Windows Server (2023 or 2025, I think.) In the old days, e.g., JVM decided for |
… -- REVERT Logs the applied-rule sequence + proof stats + line separator per case so the Windows-vs-ubuntu CI output can be diffed to find where automatic proof search diverges. To be reverted once the cause is found. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ect#3657) -- REVERT Prints per-goal whether a JML assert/script was found, the rendered command lines (with \r/\n visualized), and any exception thrown by pse.execute, to locate the Windows-only failure. To be reverted with the JmlScriptTest one. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The reason is actually quite interesting as a reminder of the subtleties between the platforms: The problem was in SymbolicExecutionMacro: depending on the line endings "simplify\n" --> "simplify" and a later equals check to "simplify" when deciding whether to apply the taclet or not succeeded. While when the line endings in the txt file were The difference between the CI and your machine is most likely the git configuration that converts / does not convert the line endings in the files. Even so, not necessary, the fix for the deprecated ScriptLineParser is also in as additional hardening. The merge and the commit that fixes the test are now on the branch. |
SymbolicExecutionOnlyMacro read its admitted rule / rule-set lists from the
bundled .txt resources and split them on "\n". On a Windows checkout these
resources have CRLF line endings (.gitattributes marks them as text), so every
entry kept a trailing '\r' ("assignment\r", "simplify_prog\r", ...).
isAdmittedRule compares the actual rule name ("assignment") against those
entries via List.contains, which then never matched. As a result no symbolic-
execution rule was admitted, the macro applied nothing, ApplyScriptsMacro never
reached a goal carrying a JmlAssert, and all goals fell through to the
TryCloseMacro fallback -- making JmlScriptTest cases close (AutoOnly2) or fail
to close (NestedAssert, ObtainFromGoal) only on Windows.
Read the lists via String.lines() and strip each entry so the names match
regardless of the checkout's line endings. Reproduced locally by converting the
two resources to CRLF (3 cases fail), fixed by this change (all 7 pass).
with AI tooling support
4 participants
Related Issue
For quite some time, we have a prototype for JML proof scripts which we finally want to bring to the mater branch.
Intended Change
Proof scripts can be written into JML comments and can be obeyed during automatic verification.
The major benefit is that the localisation of the proof node to which a proof script should be applied is natural.
The other benefit is that one can use JML expressions and thus does not have to leave the realm of JML to do script-guided proofs.
This relies on #3587 and needs #3654 merged.
Plan
Type of pull request
Ensuring quality
WIP:
Additional information and contact(s)
Planned to be done Mid 09/25
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.