Skip to content

Comments

Fix (sc)tptp output when the problem file is in cnf#61

Open
jcailler wants to merge 2 commits intoGoelandProver:masterfrom
jcailler:fix-otptp-cnf
Open

Fix (sc)tptp output when the problem file is in cnf#61
jcailler wants to merge 2 commits intoGoelandProver:masterfrom
jcailler:fix-otptp-cnf

Conversation

@jcailler
Copy link
Member

@jcailler jcailler commented Aug 25, 2025

Bug fix

Description

Fix the (sc)tptp output when the given problem file is in cnf

Test-suite update

  • Add bugs/bug_61.p (in master, this problem panics with -proof when it shouldn't).

@jcailler jcailler requested a review from jrosain August 25, 2025 07:42
@github-actions github-actions bot added the needs:ci Needs a CI run before merging label Aug 25, 2025
@jcailler jcailler added part:plugins The PR is about plugin-related code kind:fix The PR fixes a bug labels Aug 25, 2025
@jcailler jcailler added this to the 1.2 milestone Aug 25, 2025
@jrosain jrosain added the request:ci Requests a CI run from the workflow label Aug 25, 2025
@github-actions github-actions bot removed the request:ci Requests a CI run from the workflow label Aug 25, 2025
@jrosain
Copy link
Member

jrosain commented Aug 25, 2025

Can you update the test suite with the bug please?

@jrosain
Copy link
Member

jrosain commented Aug 25, 2025

Where is the bug exactly? The file you provided outputs "VALID" in the master version so I'm pretty sure an additional check is missing here

EDIT: I guess that you want to add the -otptp flag to the problem.

@jrosain
Copy link
Member

jrosain commented Aug 25, 2025

By the way, this is a bug file so it should go in the bug folder under the name bug_61.p

@jcailler
Copy link
Member Author

By the way, this is a bug file so it should go in the bug folder under the name bug_61.p

I though the bug/ fold was for current bugs, not solved ones?

@jrosain
Copy link
Member

jrosain commented Aug 25, 2025

No, it is for solved ones so that it doesn't happen again and we have a pointer from the original bug / where they were fixed.

@jrosain jrosain added the request:ci Requests a CI run from the workflow label Aug 25, 2025
@github-actions github-actions bot removed the request:ci Requests a CI run from the workflow label Aug 25, 2025
@jrosain
Copy link
Member

jrosain commented Aug 25, 2025

This fails locally but not in the actions. See #62.

parser = Parser(f)

if any(out in parser.arguments for out in outputTest) :
if any(out in parser.arguments for out in outputTest) and (os.path.exists(os.path.splitext(f)[0] + ".out")) :
Copy link
Member

Choose a reason for hiding this comment

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

It'd be great to simply check if a .out exists in this case and remove the option check!

Copy link
Member

Choose a reason for hiding this comment

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

(I'm requesting the CI as I don't think any change in a .go file is needed)

@jrosain jrosain added the request:ci Requests a CI run from the workflow label Aug 29, 2025
@github-actions github-actions bot removed needs:ci Needs a CI run before merging request:ci Requests a CI run from the workflow labels Aug 29, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

kind:fix The PR fixes a bug part:plugins The PR is about plugin-related code

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants