Port to `HB.lock` by pi8027 · Pull Request #144 · math-comp/finmap

pi8027 · 2025-10-01T16:26:55Z

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 · 2025-10-17T12:10:30Z

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

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

pi8027 · 2025-10-20T18:32:53Z

finmap.v

-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.


They should probably be deprecated first.

pi8027 · 2025-10-20T18:33:09Z

finmap.v

-Canonical imfset_unlock k := Unlockable (Imfset.imfsetE k).
-Canonical imfset2_unlock k := Unlockable (Imfset.imfset2E k).


pi8027 · 2025-10-20T18:33:52Z

finmap.v

-Module FinSupp : FinSuppSig.
-Definition fs := (fun K V d f => domf (@fmap_of_fsfun K V d f)).
-Definition E := erefl fs.
-End FinSupp.


pi8027 · 2025-10-20T18:33:57Z

finmap.v

-Definition E := erefl fs.
-End FinSupp.
-Notation finsupp := FinSupp.fs.
-Canonical unlockable_finsupp := Unlockable FinSupp.E.


pi8027 · 2025-10-20T18:34:40Z

finmap.v

-End FsfunSig.
-End FsfunSig.
-
-Module Fsfun : FsfunSig.


pi8027 · 2025-10-20T18:35:28Z

finmap.v

-Canonical fsfun_of_funE K V default S h key x :=
-   Unlockable (@Fsfun.of_ffunE K V default S h key x).


pi8027 · 2025-10-20T18:55:06Z

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

Adapt to math-comp/finmap#144

pi8027 · 2025-10-20T21:34:32Z

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 · 2025-10-21T13:47:59Z

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 · 2025-10-21T23:23:08Z

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 · 2025-10-22T11:36:16Z

finmap.v

  _ : canonical_keys enum_fset
 }.

+#[deprecated(since="finmap 2.3.0", note="Use finSet instead")]


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

Sounds reasonable

Remove unnecessary %fmap

0d12812

pi8027 force-pushed the cleanup-phant branch from 02b0059 to e20db47 Compare October 20, 2025 18:28

pi8027 changed the title ~~Remove the use of the phantom type~~ Port to HB.lock Oct 20, 2025

pi8027 commented Oct 20, 2025

View reviewed changes

pi8027 added a commit to math-comp/multinomials that referenced this pull request Oct 20, 2025

Adapt to math-comp/finmap#144

d1a3e32

pi8027 added a commit to math-comp/multinomials that referenced this pull request Oct 20, 2025

Adapt to math-comp/finmap#144

3a73528

pi8027 added a commit to math-comp/multinomials that referenced this pull request Oct 20, 2025

Merge pull request #118 from math-comp/finmap144

dfbb14f

Adapt to math-comp/finmap#144

pi8027 marked this pull request as draft October 20, 2025 21:20

pi8027 force-pushed the cleanup-phant branch from e20db47 to 62cb478 Compare October 20, 2025 21:29

pi8027 marked this pull request as ready for review October 20, 2025 21:30

pi8027 requested a review from CohenCyril October 20, 2025 21:34

pi8027 marked this pull request as draft October 21, 2025 14:55

pi8027 force-pushed the cleanup-phant branch from b5cffc4 to a1d6e52 Compare October 21, 2025 23:15

pi8027 marked this pull request as ready for review October 21, 2025 23:23

Remove the use of the phantom type

a212a4f

pi8027 force-pushed the cleanup-phant branch from a1d6e52 to b111d2e Compare October 21, 2025 23:37

pi8027 commented Oct 22, 2025

View reviewed changes

pi8027 added 2 commits October 23, 2025 18:58

Use HB.lock

2e0befd

Update Docker CI

6c4d7de

pi8027 force-pushed the cleanup-phant branch from b111d2e to 6c4d7de Compare October 23, 2025 16:59

		Canonical imfset_unlock k := Unlockable (Imfset.imfsetE k).
		Canonical imfset2_unlock k := Unlockable (Imfset.imfset2E k).

		Canonical fsfun_of_funE K V default S h key x :=
		Unlockable (@Fsfun.of_ffunE K V default S h key x).

Conversation

pi8027 commented Oct 1, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

pi8027 commented Oct 17, 2025

Uh oh!

pi8027 left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

pi8027 commented Oct 20, 2025

Uh oh!

pi8027 commented Oct 20, 2025

Uh oh!

pi8027 commented Oct 21, 2025

Uh oh!

pi8027 commented Oct 21, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

pi8027 commented Oct 1, 2025 •

edited

Loading

pi8027 left a comment •

edited

Loading