Skip to content

Cleanup: replace *FormList by Lib.List[Form]#46

Open
jrosain wants to merge 3 commits intoGoelandProver:masterfrom
jrosain:remove-more-pointers
Open

Cleanup: replace *FormList by Lib.List[Form]#46
jrosain wants to merge 3 commits intoGoelandProver:masterfrom
jrosain:remove-more-pointers

Conversation

@jrosain
Copy link
Member

@jrosain jrosain commented Jul 20, 2025 •
edited
Loading

Removed FormList and replaced everything with Lib.List[Form].

This makes us win between 5 and 10s on SYN007+1.014.p on my machine.

PR dependencies

@github-actions github-actions bot added the needs:ci Needs a CI run before merging label Jul 20, 2025
@jrosain jrosain requested a review from jcailler July 20, 2025 10:08
@jrosain jrosain added kind:cleanup Refactoring or improvement of existing code has:other-pr-dependency This PR cannot be merged before another PR (the maintainer should specify the dependency(ies)) request:ci Requests a CI run from the workflow labels Jul 20, 2025
@jrosain jrosain added this to the 1.2 milestone Jul 20, 2025
@github-actions github-actions bot removed request:ci Requests a CI run from the workflow needs:ci Needs a CI run before merging labels Jul 20, 2025
@jrosain jrosain added the needs:rebase When the PR needs to get rebased in order to get merged label Jul 23, 2025
@jrosain jrosain force-pushed the remove-more-pointers branch from 48f6ade to 762cee0 Compare July 25, 2025 13:05
@github-actions github-actions bot added the needs:ci Needs a CI run before merging label Jul 25, 2025
@jrosain jrosain added request:ci Requests a CI run from the workflow and removed needs:rebase When the PR needs to get rebased in order to get merged labels Jul 25, 2025
@github-actions github-actions bot removed request:ci Requests a CI run from the workflow needs:ci Needs a CI run before merging labels Jul 25, 2025
@jrosain jrosain removed the has:other-pr-dependency This PR cannot be merged before another PR (the maintainer should specify the dependency(ies)) label Jul 26, 2025
@jrosain jrosain mentioned this pull request Jul 27, 2025
Open
@jrosain jrosain force-pushed the remove-more-pointers branch from 762cee0 to 80a21ba Compare July 27, 2025 12:55
@github-actions github-actions bot added the needs:ci Needs a CI run before merging label Jul 27, 2025
@jrosain jrosain added the has:other-pr-dependency This PR cannot be merged before another PR (the maintainer should specify the dependency(ies)) label Jul 27, 2025
@jcailler jcailler added the needs:rebase When the PR needs to get rebased in order to get merged label Jul 27, 2025
@jrosain jrosain force-pushed the remove-more-pointers branch from 80a21ba to bd2e783 Compare July 27, 2025 18:19
@jrosain jrosain added request:ci Requests a CI run from the workflow and removed has:other-pr-dependency This PR cannot be merged before another PR (the maintainer should specify the dependency(ies)) needs:rebase When the PR needs to get rebased in order to get merged labels Jul 27, 2025
@github-actions github-actions bot removed request:ci Requests a CI run from the workflow needs:ci Needs a CI run before merging labels Jul 27, 2025
@jrosain jrosain force-pushed the remove-more-pointers branch from bd2e783 to 109a9fe Compare August 26, 2025 08:26
@github-actions github-actions bot added the needs:ci Needs a CI run before merging label Aug 26, 2025
@jrosain jrosain added request:ci Requests a CI run from the workflow and removed needs:ci Needs a CI run before merging request:ci Requests a CI run from the workflow labels Aug 26, 2025
@jcailler jcailler added the needs:rebase When the PR needs to get rebased in order to get merged label Aug 29, 2025
@jrosain jrosain force-pushed the remove-more-pointers branch from 109a9fe to b33e6ae Compare August 29, 2025 13:22
@jrosain jrosain removed the needs:rebase When the PR needs to get rebased in order to get merged label Aug 29, 2025
@github-actions github-actions bot added the needs:ci Needs a CI run before merging label Aug 29, 2025
@jrosain jrosain added the request:ci Requests a CI run from the workflow label Aug 29, 2025
@github-actions github-actions bot removed request:ci Requests a CI run from the workflow needs:ci Needs a CI run before merging labels Aug 29, 2025
@jcailler
Copy link
Member

jcailler commented Jan 25, 2026 •
edited
Loading

The Rocq output for SYN007+1.014.p doesn't work anymore with this PR (memory issues, the process is killed).

@jrosain jrosain mentioned this pull request Feb 7, 2026
Open
@jrosain
Copy link
Member Author

jrosain commented Feb 7, 2026

I'm backporting the issue over here.

The following problems produces an error when trying to export the Rocq proof in inner skolemization:

  • SYN325
  • SYN340
  • SYN341
  • SYN369
  • SYN947

jrosain
jrosain commented Feb 7, 2026
View reviewed changes
src/Mods/rocq/proof.go
Comment on lines +105 to +116
target := Lib.ListIndexOf(proof.GetTargetForm(), hypotheses)
var actualTarget int
switch t := target.(type) {
case Lib.Some[int]:
actualTarget = t.Val
case Lib.None[int]:
Glob.Anomaly("coq", fmt.Sprintf(
"Index of %s not found in %s",
proof.GetTargetForm().ToString(),
Lib.ListToString(hypotheses, ", ", "[]"),
))
}
Copy link
Member Author

@jrosain jrosain Feb 7, 2026

Choose a reason for hiding this comment

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

Looks like the issue comes from here: we now check whether the formula is found or not.

This is probably a bug that comes from deeper (i.e., most likely from the deskolemization algorithm). We should probably bear with it until the rework of the deskolemization algorithm.

@jrosain
Copy link
Member Author

jrosain commented Feb 7, 2026

We should probably create an issue about that when this PR is merged.

@github-actions github-actions bot added the needs:ci Needs a CI run before merging label Feb 7, 2026
@jrosain
Copy link
Member Author

jrosain commented Feb 7, 2026

The Rocq output for SYN007+1.014.p doesn't work anymore with this PR (memory issues, the process is killed).

Fixed.

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

Reviewers

@jcailler jcailler Awaiting requested review from jcailler

At least 1 approving review is required to merge this pull request.

Assignees

@jcailler jcailler

Labels

kind:cleanup Refactoring or improvement of existing code

Projects

None yet

Milestone

1.2

Development

Successfully merging this pull request may close these issues.

2 participants

@jrosain @jcailler