Starting port to HB

[CohenCyril]

Files available for porting ([x] means taken by someone)

• [ ] topology.v (look for TODO_HB)
• [ ] normedtype.v (look for TODO_HB)

Motivation for this change

@affeldt-aist @gares @proux01 @mkerjean port of MCA in progress (see .nix/config.nix for the requirements)

Things done/to do

• [ ] added corresponding entries in CHANGELOG_UNRELEASED.md (do not edit former entries, only append new ones, be careful: merge and rebase have a tendency to mess up CHANGELOG_UNRELEASED.md)
• [ ] added corresponding documentation in the headers

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[proux01]

I needed to add a Nix overlay to let Nix know about the mathcomp -> HB dependency, then

nix-shell --argstr bundle "8.15" --argstr job "mathcomp-analysis"  

should work

[CohenCyril]

I needed to add a Nix overlay to let Nix know about the mathcomp -> HB dependency, then

nix-shell --argstr bundle "8.15" --argstr job "mathcomp-analysis"  

Oh did I forget to commit something?

[proux01]

@CohenCyril I'll need your help here, this is stuck on a HB.instance failing with message

HB: cannot inhabit mixin Order_POrder_IsLattice on set T

which I don't understand (c.f. last FIXME in classical_sets.v)

[proux01]

Fixed, there was a missing instance. I wonder whether this should be considered a bug of HB though?

(* works *)
Check [the choiceType of set T].

(* works (no evar) *)
Check Order.IsMeetJoinDistrLattice.Build set_display (set T)
    le_def lt_def (@setIC _) (@setUC _) (@setIA _) (@setUA _)
    joinKI meetKU (@setIUl _) setIid.

(* fails: "Error: HB: cannot inhabit mixin Order_POrder_IsLattice on set T" *)
Fail #[export]
HB.instance Definition _ :=
  Order.IsMeetJoinDistrLattice.Build set_display (set T)
    le_def lt_def (@setIC _) (@setUC _) (@setIA _) (@setUA _)
    joinKI meetKU (@setIUl _) setIid.

#[export]
HB.instance Definition _ : Choice (set T) := Choice.copy _ (set T).

(* now works *)
#[export]
HB.instance Definition _ :=
  Order.IsMeetJoinDistrLattice.Build set_display (set T)
    le_def lt_def (@setIC _) (@setUC _) (@setIA _) (@setUA _)
    joinKI meetKU (@setIUl _) setIid.

More generally: shouldn't an HB.instance that doesn't instantiate any structure be an error? (I often do the mistake and then fail to realize I forgot to instantiante a previous structure).

[CohenCyril]

More generally: shouldn't an HB.instance that doesn't instantiate any structure be an error? (I often do the mistake and then fail to realize I forgot to instantiante a previous structure).

No, it should not, since adding new structures in the middle of the hierarchy might make some HB.instance redundant (hence no new instance is created) for which we do not want to raise error for backward compatibility reasons. We could raise a warning though, to bring some attention, either to the user who ports a library to a new hierarchy, or for your usecase.

[affeldt-aist]

Just for information. Compilation fails on my side at FilteredEntourage_IsUniform [1] while it looks like it should be going a bit further. It is actually the second time that I observe such a discrepancy. I thought that using nix-shell would guarantee exactly the same environment. Is it wrong?

-- [1]

Error:
HB: cannot infer some information in 
ParameterM : Type
Parameterlocal_mixin_choice_HasChoice : HasChoice.axioms_ elpi_ctx_entry_0_
Parameterlocal_mixin_eqtype_HasDecEq : Equality.mixin_of elpi_ctx_entry_0_
Parameterlocal_mixin_classical_sets_IsPointed : IsPointed.axioms_ elpi_ctx_entry_0_ elpi_ctx_entry_1_ elpi_ctx_entry_2_
Parameterlocal_mixin_topology_IsFiltered : IsFiltered.axioms_ elpi_ctx_entry_0_ elpi_ctx_entry_0_
Parameterlocal_mixin_topology_HasEntourage : HasEntourage.axioms_ elpi_ctx_entry_0_
axioms_ : Type := Axioms_ {
  uniform_ax1 : Filter entourage;
  uniform_ax2 : forall A : ?elpi_evar * ?elpi_evar -> Prop,
entourage A -> [set xy | xy.1 = xy.2] `<=` A;
  uniform_ax3 : forall A : ?elpi_evar0 * ?elpi_evar0 -> Prop,
entourage A -> entourage (A^-1)%classic;
  uniform_ax4 : forall A : ?elpi_evar1 * ?elpi_evar1 -> Prop,
entourage A ->
exists2 B : ?elpi_evar1 * ?elpi_evar1 -> Prop, entourage B & B \o B `<=` A;
  uniform_ax5 : nbhs = nbhs_ entourage;
}

[proux01]

@affeldt-aist no, that's also what I'm experiencing with

nix-shell --arg withEmacs true --argstr bundle "8.16" --argstr job "mathcomp-analysis"

I indeed got further but realized I made something slightly wrong an went back "fixing" it. That's when I encoutered this issue and stopped there. Sorry, I should have put an explanatory comment.

[proux01]

@CohenCyril @affeldt-aist I put a list of files currently needing porting / with someone working on them in the description of the PR on top, please edit as files become available / check boxes when you are working on one

[CohenCyril]

I would also put the name of the person working on it on the side.

[affeldt-aist]

I haven't figured out weak_topologicalTypeMixin but maybe at least nbhs_of_open that will be used ought better be outisde of a builders section to stay accessible.

[proux01]

It seems that often, the complicated Definition foo_mixin without a Canonical foo_type := FooType foo_mixin just after should become HB factories and builders (but that's sometimes easier to say than to do).

[CohenCyril]

I haven't figured out weak_topologicalTypeMixin b

I have, I will post it soon or I can show you.

[CohenCyril]

@affeldt-aist @proux01 in order to fix the product_topology bit I need to have the canonical pointed type on a dependent product, so I committed only the weak and sup topology and I will investigate or workaround the issue on dependent products.

[proux01]

measure.v was fairly easy to port. But I encountered some Qed failures, apparently when using congr (lim _), I should investigate.

[proux01]

Rebased and force pushed to trigger the CI.

[proux01]

FYI, CI is green on 8.15, 8.16 and master (of course, there are still a few things commented out in topology.v).

[zstone1]

FYI, I've merged several results (metrics for supremums and quotients) in the last few days that involve some mixins. Just a heads up to A) Expect the rebase of topology.v to not build correctly the first time B) Reach out to me if you run into any issues porting these changes I'm happy to do whatever is helpful. I just want to make ensure I'm not duplicating or interfering with your work.

[proux01]

Thanks for the head up @zstone1 ! As @CohenCyril said, the HB port shouldn't hinder further development in the main branch, so your changes are fine. Of course, if at some point you want to help completing the HB port (you are probably the best expert of the part of the code that remains to port), that would be welcome, but certainly not an obligation.

[zstone1]

I'd be happy to make an attempt at porting the rest. I have some free time coming up, so I should be able to make some progress. What would help me a lot:

1. Any blockers? For example, things that we know need corresponding updates in HB itself.
2. Any changes to the math? For example, do you expect any definitions to change in edge cases?
3. Any areas I shouldn't touch?
4. In terms of git management, my plan is to duplicate this branch in my fork, and then make PRs against this branch (rather than master) is that the right approach?

I think the first step is a rebase, which might be challenging in its own right.

[CohenCyril]

@affeldt-aist and I suggest we have a meeting about this port, I'm stuck in the middle of a problem of topology and I could use your advice @zstone1. Let's try to find a date. (@affeldt-aist do you want to try to do this while you're still in the french timezone?)

[affeldt-aist]

(@affeldt-aist do you want to try to do this while you're still in the french timezone?)

This is a good idea.

[zstone1]

Yeah, I'd love to help here. A couple things

• Let me know what day works. I'm taking the next couple weeks off work anyway, so I'm pretty free.
• I tried to build this branch, but discovered I'm the only one using vscoq. I can use the nix-shell to make just fine. But vscoq doesn't use the right nix artifacts. I'll figure something out.

[proux01]

Since we are no longer handling the HB port as a PR, try to close this to try to get CI on the branch.

[proux01]

Ok, so we don't have CI on this branch. I suggest to push to the HB branch via PRs targetting it and hopefully we'll get CI in the PRs.