Skip to content

Improve Inference Testing, THF_plain Translation, and Dependency Diagnostics#545

Merged
apease merged 23 commits into
masterfrom
development
Jun 22, 2026
Merged

Improve Inference Testing, THF_plain Translation, and Dependency Diagnostics#545
apease merged 23 commits into
masterfrom
development

Conversation

@ShaunRose

Copy link
Copy Markdown
Member
  • Updated Vampire integration to use TPTP includes instead of concatenating temporary combined files.
  • Fixed inference test constituent path parsing, stale file detection, and success checking logic.
  • Improved HOL and THF translation behavior, including fixes for ExprToTHF and THF_plain parsing.
  • Added inference test suite dashboard counts for total tests, queued tests, passed tests, and failed tests.
  • Added meta predicates for inference test options including language, timeout, CWA, modus ponens, drop-one-premise, and HOL modal handling.
  • Added variable-arity relation generation to FormulaPreprocessorTest.testGatherRelationships().
  • Fixed case elimination behavior used by tests such as TQG25.kif.tq.
  • Improved unloaded constituent diagnostics and added a button to generate the unloaded term dependency cache.
  • Updated browse formula links to open the editor directly at the referenced source line.
  • Removed unnecessary TFF comments and cleaned up logging by replacing System.out usage with LoggingUtils.log.
  • Added a button for term_dependency.ser generation in Diagnostics.jsp.
  • Added salted password hashing support for improved user authentication security.
  • Resolved merge conflicts and updated related tests for expanded relationship gathering.

ShaunRose and others added 23 commits June 10, 2026 12:21
… Formula now defaults to 7 but can be set from the preference maxPredicateArity, Added config_full for missing constituent dependency diagnostics to run using -a flag
…pend upon onfig_full.xml, now it just finds all the kif files in KBs and temporarily loads those as constituents if the term_dependency.ser file does not already exist
…doing it automatically during initialization
@github-actions

Copy link
Copy Markdown

Qodana for JVM

It seems all right 👌

No new problems were found according to the checks applied

💡 Qodana analysis was run in the pull request mode: only the changed files were checked

View the detailed Qodana report

To be able to view the detailed Qodana report, you can either:

To get *.log files or any other Qodana artifacts, run the action with upload-result option set to true,
so that the action will upload the files as the job artifacts:

      - name: 'Qodana Scan'
        uses: JetBrains/qodana-action@v2024.2.5
        with:
          upload-result: true
Contact Qodana team

Contact us at qodana-support@jetbrains.com

@apease apease merged commit e07b4f6 into master Jun 22, 2026
5 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants