List view

Update PR instructions in CONTRIBUTING.md

kind:documentationEnhance or add documentationEnhance or add documentation

part:infrastructureThe PR is on non-goéland codeThe PR is on non-goéland code

Status: Open (in progress).

GoelandProver/Goelandnumber 31

#31 In GoelandProver/Goeland;

· jcailler opened on Jul 10, 2025

GS3 failure: tried to apply a missing hypothesis when using <code>-inner</code> and <code>-preinner</code> flags

kind:bugSomething isn't workingSomething isn't working

part:pluginsThe PR is about plugin-related codeThe PR is about plugin-related code

Status: Open.

#16 In GoelandProver/Goeland;

· jrosain opened on May 17, 2025

Panic: invalid memory address or nil pointer dereference on typing a TFF1 problem / TFF1 proof search is not handled

kind:bugSomething isn't workingSomething isn't working

part:typingThe PR is about typed terms/the typing algorithmThe PR is about typed terms/the typing algorithm

Status: Open.

#38 In GoelandProver/Goeland;

· jrosain opened on Jul 19, 2025

Cleanup: replace <code>*FormList</code> by <code>Lib.List[Form]</code>

kind:cleanupRefactoring or improvement of existing codeRefactoring or improvement of existing code

Status: Open (in progress).

GoelandProver/Goelandnumber 46

#46 In GoelandProver/Goeland;

· jrosain opened on Jul 20, 2025

Syntax error in Rocq output due to illegal character in skolem symbols / types

kind:bugSomething isn't workingSomething isn't working

part:rocq-outputAbout the certified output in RocqAbout the certified output in Rocq

Status: Open.

#52 In GoelandProver/Goeland;

· jrosain opened on Jul 26, 2025

Major overhaul of the type system to manage typed proof search with an easier-to-maintain and less invasive API

has:other-pr-dependencyThis PR cannot be merged before another PR (the maintainer should specify the dependency(ies))This PR cannot be merged before another PR (the maintainer should specify the dependency(ies))

kind:cleanupRefactoring or improvement of existing codeRefactoring or improvement of existing code

kind:enhancementNew feature or upgrade of a previous oneNew feature or upgrade of a previous one

kind:fixThe PR fixes a bugThe PR fixes a bug

part:proof-searchThe PR is about the proof-search algorithmThe PR is about the proof-search algorithm

part:typingThe PR is about typed terms/the typing algorithmThe PR is about typed terms/the typing algorithm

part:unificationAbout the unification process of GoélandAbout the unification process of Goéland

Status: Open (in progress).

GoelandProver/Goelandnumber 53

#53 In GoelandProver/Goeland;

· jrosain opened on Jul 27, 2025

Fix syntax error on Rocq output by using a better printing system

has:other-pr-dependencyThis PR cannot be merged before another PR (the maintainer should specify the dependency(ies))This PR cannot be merged before another PR (the maintainer should specify the dependency(ies))

kind:cleanupRefactoring or improvement of existing codeRefactoring or improvement of existing code

kind:enhancementNew feature or upgrade of a previous oneNew feature or upgrade of a previous one

kind:fixThe PR fixes a bugThe PR fixes a bug

needs:ciNeeds a CI run before mergingNeeds a CI run before merging

part:rocq-outputAbout the certified output in RocqAbout the certified output in Rocq

Status: Open (in progress).

GoelandProver/Goelandnumber 59

#59 In GoelandProver/Goeland;

· jrosain opened on Jul 29, 2025

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

kind:fixThe PR fixes a bugThe PR fixes a bug

part:pluginsThe PR is about plugin-related codeThe PR is about plugin-related code

Status: Open (in progress).

GoelandProver/Goelandnumber 61

#61 In GoelandProver/Goeland;

· jcailler opened on Aug 25, 2025

Remove <code>PrintError</code> API and always call to <code>Fatal</code> or <code>Anomaly</code> instead

kind:cleanupRefactoring or improvement of existing codeRefactoring or improvement of existing code

part:loggingThe PR/issue is about loggingThe PR/issue is about logging

Status: Open (in progress).

GoelandProver/Goelandnumber 57

#57 In GoelandProver/Goeland;

· jrosain opened on Jul 27, 2025

Add <code>IProof</code> interface with a tree structure and add relevant adapter for <code>[]Search.ProofStruct</code>

has:other-pr-dependencyThis PR cannot be merged before another PR (the maintainer should specify the dependency(ies))This PR cannot be merged before another PR (the maintainer should specify the dependency(ies))

kind:enhancementNew feature or upgrade of a previous oneNew feature or upgrade of a previous one

needs:ciNeeds a CI run before mergingNeeds a CI run before merging

part:proof-outputAbout the vanilla proof output (in custom format)About the vanilla proof output (in custom format)

Status: Open (in progress).

GoelandProver/Goelandnumber 64

#64 In GoelandProver/Goeland;

· jrosain opened on Sep 1, 2025