Skip to content

Taclet definition added to problemHeader#3733

Open
wadoon wants to merge 1 commit intomainfrom
weigl/fix849
Open

Taclet definition added to problemHeader#3733
wadoon wants to merge 1 commit intomainfrom
weigl/fix849

Conversation

@wadoon
Copy link
Member

@wadoon wadoon commented Feb 7, 2026

Related Issue

This pull request resolves #849 .

Intended Change

Compute a proper problem header including also the taclets and all other definitions.

The problem header is delivered through the initConfig, which may be problematic.

Plan

  • fixing it

Type of pull request

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

Ensuring quality

  • I made sure that introduced/changed code is well documented (javadoc and inline comments).
    IT IS TOO LATE FOR JAVADOC *yawn*

  • I have tested the feature as follows: by hand

@wadoon wadoon added this to the v3.0.0 milestone Feb 7, 2026
@wadoon wadoon requested a review from unp1 February 7, 2026 00:52
@wadoon wadoon self-assigned this Feb 7, 2026
@wadoon wadoon changed the title compute a proper problem header including also the taclets Taclet definition added to problemHeader Feb 7, 2026
@unp1
Copy link
Member

unp1 commented Feb 7, 2026

Thanks. At the moment I get exception when saving aproof that was started not via a .key file but by selecting a directory and choosing a proof obligation.

Steps to reproduce:

  • File > Open:
    • Navigate to examples/firstTouch/06-BinarySearch
    • Select the src/ folder
  • Run the proof
  • Saving the completed proof results in the error message "No proof present"

@wadoon
Copy link
Member Author

wadoon commented Feb 7, 2026

Thanks. At the moment I get exception when saving aproof that was started not via a .key file but by selecting a directory and choosing a proof obligation.

Should be resolved. NPE during saving as the header variable is null, as these proofs are not obtained by reading a KeY-file.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

problem with loading proofs containing non-axiom (user defined) taclets

2 participants