Skip to content

Port to HB.lock #144

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
wants to merge 4 commits into
base: master
Choose a base branch
from
Open

Port to HB.lock #144

wants to merge 4 commits into from

Conversation

@pi8027
Copy link
Member

@pi8027 pi8027 commented Oct 1, 2025 •
edited
Loading

This PR:

  • removes the use of phantom types, and
  • ports the keyed- and module-locking to HB.lock.

Note that unlocking fsfun_of_ffun does not give the same result as before (because it was implemented in a weird way). We need to use fsfun_ffun instead.

@pi8027
Copy link
Member Author

pi8027 commented Oct 17, 2025

FTR, Cyril's feedback on locking was that we should probably switch from keyed locking to module locking (like HB.lock). We can still keep the key by module-locking the definitions that take the key.

@pi8027 pi8027 changed the title Remove the use of the phantom type Port to HB.lock Oct 20, 2025
pi8027
pi8027 commented Oct 20, 2025
View reviewed changes
Copy link
Member Author

@pi8027 pi8027 left a comment •
edited
Loading

Choose a reason for hiding this comment

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

FTR, a few deprecation constants are missing for the moment, but I'm unsure if we want to be that strict or not.

finmap.v
Comment on lines 758 to 763
Module Imfset : ImfsetSig.
Definition imfset key := imfset_def key.
Definition imfset2 key := imfset2_def key.
Lemma imfsetE key : imfset key = imfset_def key. Proof. by []. Qed.
Lemma imfset2E key : imfset2 key = imfset2_def key. Proof. by []. Qed.
End Imfset.
Copy link
Member Author

@pi8027 pi8027 Oct 20, 2025

Choose a reason for hiding this comment

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

They should probably be deprecated first.

Copy link
Member Author

@pi8027 pi8027 Oct 23, 2025

Choose a reason for hiding this comment

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

Done.

finmap.v
Comment on lines -770 to -771
Canonical imfset_unlock k := Unlockable (Imfset.imfsetE k).
Canonical imfset2_unlock k := Unlockable (Imfset.imfset2E k).
Copy link
Member Author

@pi8027 pi8027 Oct 20, 2025

Choose a reason for hiding this comment

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

Same?

finmap.v
Comment on lines 3769 to 3772
Module FinSupp : FinSuppSig.
Definition fs := (fun K V d f => domf (@fmap_of_fsfun K V d f)).
Definition E := erefl fs.
End FinSupp.
Copy link
Member Author

@pi8027 pi8027 Oct 20, 2025

Choose a reason for hiding this comment

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

Same?

Copy link
Member Author

@pi8027 pi8027 Oct 23, 2025

Choose a reason for hiding this comment

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

Done.

finmap.v
Definition E := erefl fs.
End FinSupp.
Notation finsupp := FinSupp.fs.
Canonical unlockable_finsupp := Unlockable FinSupp.E.
Copy link
Member Author

@pi8027 pi8027 Oct 20, 2025

Choose a reason for hiding this comment

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

Same?

finmap.v
End FsfunSig.
End FsfunSig.

Module Fsfun : FsfunSig.
Copy link
Member Author

@pi8027 pi8027 Oct 20, 2025

Choose a reason for hiding this comment

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

Same?

Copy link
Member Author

@pi8027 pi8027 Oct 23, 2025

Choose a reason for hiding this comment

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

Done.

finmap.v
Comment on lines -3893 to -3894
Canonical fsfun_of_funE K V default S h key x :=
Unlockable (@Fsfun.of_ffunE K V default S h key x).
Copy link
Member Author

@pi8027 pi8027 Oct 20, 2025

Choose a reason for hiding this comment

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

Same?

pi8027 added a commit to math-comp/multinomials that referenced this pull request Oct 20, 2025
@pi8027
Adapt to math-comp/finmap#144
d1a3e32
pi8027 added a commit to math-comp/multinomials that referenced this pull request Oct 20, 2025
@pi8027
Adapt to math-comp/finmap#144
3a73528
@pi8027
Copy link
Member Author

pi8027 commented Oct 20, 2025

The breakage of multinomials should be fixed by math-comp/multinomials#118.

pi8027 added a commit to math-comp/multinomials that referenced this pull request Oct 20, 2025
@pi8027
Merge pull request #118 from math-comp/finmap144
dfbb14f 
Adapt to math-comp/finmap#144
@pi8027 pi8027 marked this pull request as draft October 20, 2025 21:20
@pi8027 pi8027 marked this pull request as ready for review October 20, 2025 21:30
@pi8027
Copy link
Member Author

pi8027 commented Oct 20, 2025

In the end, locking fun_of_fsfun does not seem to fix the issue in multinomials. So, I leave it unlocked here. In any case, this PR reduces some boilerplate code.

@pi8027 pi8027 requested a review from CohenCyril October 20, 2025 21:34
@pi8027
Copy link
Member Author

pi8027 commented Oct 21, 2025

T in {fset T} is not interpreted in type_scope anymore. I will fix it. (It would be better if we address math-comp/math-comp#1136 though.)

@pi8027 pi8027 marked this pull request as draft October 21, 2025 14:55
@pi8027
Copy link
Member Author

pi8027 commented Oct 21, 2025

T in {fset T} is not interpreted in type_scope anymore. I will fix it. (It would be better if we address math-comp/math-comp#1136 though.)

Fixed.

@pi8027 pi8027 marked this pull request as ready for review October 21, 2025 23:23
pi8027
pi8027 commented Oct 22, 2025
View reviewed changes
finmap.v
_ : canonical_keys enum_fset
}.

#[deprecated(since="finmap 2.3.0", note="Use finSet instead")]
Copy link
Member Author

@pi8027 pi8027 Oct 22, 2025

Choose a reason for hiding this comment

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

Since this change is neither a bug fix nor an adaptation to recent versions of Rocq/MathComp, I suggest incrementing the minor version for the next release. @proux01

Copy link
Contributor

@proux01 proux01 Oct 22, 2025

Choose a reason for hiding this comment

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

Sounds reasonable

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

Reviewers

@proux01 proux01 proux01 left review comments

@CohenCyril CohenCyril Awaiting requested review from CohenCyril

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@pi8027 @proux01