Skip to content
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.

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

Port to HB #698

Closed
wants to merge 40 commits into from
Closed

Port to HB #698

wants to merge 40 commits into from

Conversation

CohenCyril
Copy link
Member

@CohenCyril CohenCyril commented Jul 13, 2022

Files available for porting ([x] means taken by someone)
  • topology.v (look for TODO_HB)
  • realfun.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
Copy link
Collaborator

proux01 commented Jul 13, 2022

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
Copy link
Member Author

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
Copy link
Collaborator

proux01 commented Jul 19, 2022

@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
Copy link
Collaborator

proux01 commented Jul 20, 2022

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
Copy link
Member Author

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.

theories/topology.v Outdated Show resolved Hide resolved
@affeldt-aist
Copy link
Member

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
Copy link
Collaborator

proux01 commented Jul 26, 2022

@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
Copy link
Collaborator

proux01 commented Jul 26, 2022

@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
Copy link
Member Author

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

@affeldt-aist
Copy link
Member

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
Copy link
Collaborator

proux01 commented Jul 27, 2022

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
Copy link
Member Author

CohenCyril commented Jul 27, 2022

I haven't figured out weak_topologicalTypeMixin b

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

@CohenCyril
Copy link
Member Author

@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
Copy link
Collaborator

proux01 commented Jul 27, 2022

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

@proux01 proux01 force-pushed the hierarchy-builder branch from 9ef5ac7 to 6d5867e Compare July 29, 2022 12:18
@proux01
Copy link
Collaborator

proux01 commented Jul 29, 2022

Rebased and force pushed to trigger the CI.

@proux01
Copy link
Collaborator

proux01 commented Aug 1, 2022

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

@proux01 proux01 force-pushed the hierarchy-builder branch from 4b0233f to dcc30c9 Compare August 19, 2022 15:13
@proux01 proux01 force-pushed the hierarchy-builder branch 3 times, most recently from 2ba7e9a to ce002d6 Compare September 9, 2022 14:37
@affeldt-aist affeldt-aist marked this pull request as draft October 20, 2022 10:22
@zstone1 zstone1 mentioned this pull request Oct 26, 2022
2 tasks
@zstone1
Copy link
Contributor

zstone1 commented Feb 8, 2023

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
Copy link
Collaborator

proux01 commented Feb 9, 2023

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.

affeldt-aist and others added 17 commits March 25, 2023 09:18
* fixes

- fixes #828
- fixes #835
- fixes #838
* add a type for finite measures

- s-finite measures from branch kernels
- add subprobabilities
- dirac instance of probability
- rm finite_measure
- renaming
- minor fix
Co-authored-by: Quentin Vermande <[email protected]>
- a few pinfty/ninfty -> y/Ny renamings
* Add itv.v

Taking inspiration on signed.v, replacing sign by intervals.

* Add interval multiplication

* Add hints to automatically solve _ <= 1 goals

* Test to see if usable as a replacement for prob

* use notation from mathcomp_extra.v

* changelog and rm redundant code

* prefix duplicated identifiers

---------

Co-authored-by: Reynald Affeldt <[email protected]>
- fixes #866
- fixes #867
- fixes #868
@@ -620,9 +625,10 @@ Definition measurableTypeR := salgebraType (R.-ocitv.-measurable).
Definition measurableR : set (set R) :=
(R.-ocitv.-measurable).-sigma.-measurable.

HB.instance Definition _ := Pointed.on R.
Copy link
Member

Choose a reason for hiding this comment

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

NB: non forgetful inheritance detected

Copy link
Member

@affeldt-aist affeldt-aist Apr 5, 2023

Choose a reason for hiding this comment

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

Using measurableTypeR instead of R makes the warning disappear but causes problems later (in the sense that one needs to explicitly use measurableTypeR here and there).
Is it a case of controlled/harmless non-forgetful inheritance for which the warning should be silenced?

@@ -620,9 +625,10 @@ Definition measurableTypeR := salgebraType (R.-ocitv.-measurable).
Definition measurableR : set (set R) :=
(R.-ocitv.-measurable).-sigma.-measurable.

HB.instance Definition _ := Pointed.on R.
HB.instance Definition R_isMeasurable :
Copy link
Member

Choose a reason for hiding this comment

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

non forgetful inheritance detected

proux01 and others added 7 commits April 10, 2023 13:31
Co-authored-by: Reynald Affeldt <[email protected]>
* gen exp_fun

- rename to power_pow
- fix doc
- add scope to notation

Co-authored-by: Alessandro Bruni <[email protected]>
Co-authored-by: Takafumi Saikawa <[email protected]>

* add lemma power12_sqrt

* additional lemmas

* change power_pos so that 0^0=1

- so that power_pos and exprn coincide

* measurable_fun exp ln

* fix chaneglog

* add power_pos_intmul proposed by Pierre

* fix changelog

---------

Co-authored-by: Alessandro Bruni <[email protected]>
Co-authored-by: Takafumi Saikawa <[email protected]>
Co-authored-by: Alessandro Bruni <[email protected]>
- fixes issue #883

Co-authored-by: Alessandro Bruni <[email protected]>
Co-authored-by: Takafumi Saikawa <[email protected]>
@proux01 proux01 force-pushed the hierarchy-builder branch from 5fe9a6c to 7c4bc43 Compare April 12, 2023 11:11
@proux01
Copy link
Collaborator

proux01 commented Apr 12, 2023

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 proux01 closed this Apr 12, 2023
@proux01
Copy link
Collaborator

proux01 commented Apr 12, 2023

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement ✨ This issue/PR is about adding new features enhancing the library experiment 🧪 This issue/PR is very experimental
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants