Looking for feedback on a theorem statement

Stream: mathlib4

[Michael Novak]

Hi, I wanted to ask for feedback about the statement of a theorem I would like to prove and eventually contribute to Mathlib. I plan to write more theorems related to this subject, but I first wanted to make sure I understand the style / conventions of Mathlib. Personally I don't like how this theorem is stated very much, especially not all the many ands, but I was advised not to try to define too many structures and try to state things more directly, so that's what I try to do here. The theorem says that every regular parametrized curve has a unit speed reparametrization, i.e., reparametrization by arc-length:

theorem reparam_by_arc_length {ι : Type*} [Fintype ι] (I : Set ℝ) [I.OrdConnected] {r : WithTop ℕ∞}
  {once_diff : 1 ≤ r} (c : ℝ → EuclideanSpace ℝ ι) (hc : ContDiffOn ℝ r c I)
  (regular : ∀ t : I, deriv c t ≠ 0) :
  ∃ (φ : ℝ → ℝ) (J : Set ℝ), J.OrdConnected ∧ MonotoneOn φ J ∧ DifferentiableOn ℝ φ J
  ∧ φ '' J = I ∧ ∀ s : J, ‖deriv (c∘φ) s‖ = 1 := sorry

How would you modify it to be fit for Mathlib?

[Aaron Liu]

Is it specific to euclidean space or does it work for any real vector space or any finite dimensional real vector space or any normed real vector space or...

[Aaron Liu]

also once_diff probably shouldn't be an implicit argument since it's impossible to infer

[Michael Novak]

Aaron Liu said:

Is it specific to euclidean space or does it with for any real vector space or any finite dimensional real vector space or any normed real vector space or...

I'm not sure, but I think this might work in any normed real vector space

[Michael Novak]

In regards to the type of the theorem, i.e, the part with all the ands, do you think that's a good style? Is there a better way of doing it?

[Sébastien Gouëzel]

In the above theorem, I would make a definition arclengthReparamFrom c x₀ which would be the arclength reparameterization sending 0 to x₀. It would be defined without any assumption on c (using junk values at points where it is not well defined). And then you would state its properties, in separate lemmas. Note that it would work at once for all intervals I containing x₀ on which the function is C^1 with nonvanishing derivative.

This would be one definition (but of a function, not of a type), and many API lemmas establishing the properties of this function. Your statement above with existentials could be a technical lemma used in the proof of the properties of arclengthReparamFrom, but not the final statement as it is hard to use as you point out.

[Michael Novak]

Thank you very much! I'll try do it

[Michael Novak]

Is this a good statement of this definition (for now I still use euclidean space, but might change it later)?

def arclengthReparamFrom {I : Set ℝ} [I.OrdConnected] {ι : Type*} [Fintype ι]
  (c : ℝ → EuclideanSpace ℝ ι) (t₀ : I) : ℝ → EuclideanSpace ℝ ι := sorry

[Michael Novak]

I'm not sure if this is what you were thinking of, but I defined it like this:

noncomputable
def arclengthReparamFrom {I : Set ℝ} [I.OrdConnected] {ι : Type*} [Fintype ι]
  (c : ℝ → EuclideanSpace ℝ ι) (t₀ : I) : ℝ → EuclideanSpace ℝ ι := by
  let ψ : ℝ → ℝ := fun t ↦ ∫ τ in t₀..t, ‖deriv c τ‖
  exact c ∘ ψ⁻¹

The problem I see with this is that I would want to prove a few properties of ψ and it's inverse, in order to prove properties of the arc-length reparametrization.

[Sébastien Gouëzel]

I would rather let arclengthReparamFrom be the function ψ⁻¹, because that's the one you will use in statements. Also, there shouldn't be an I in your definition. And what exactly do you mean by ψ⁻¹?

I'd say, start with any definition you like and start proving theorems about it. You will see soon if your definition works well or if it should be tweaked.

[Michael Novak]

Sébastien Gouëzel said:

I would rather let arclengthReparamFrom be the function ψ⁻¹, because that's the one you will use in statements. Also, there shouldn't be an I in your definition. And what exactly do you mean by ψ⁻¹?

I'd say, start with any definition you like and start proving theorems about it. You will see soon if your definition works well or if it should be tweaked.

So essentially define the parameter transformation that gives us the arc-length reparametrization, i.e: φ := ψ⁻¹. Although I would also want to use properties of ψ, so maybe I should also define that before. Not sure what I would call it, but I'll think of something.

[Michael Novak]

So this is the updated definitions I came up with. Some of the names are a bit long, especially of the first definition, because I don't know what is a good description of this term - it's essentially a construction (an important one) we usually make inside a proof, I don't think there is a term for this in of itself.

import Mathlib

noncomputable section

variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℝ → E) (t₀ : ℝ)

--This is the reversed (inverse) parameter transformation for the arc-length reparametrization
def revParamTransformForArclengthReparamFrom : ℝ → ℝ :=
  fun t ↦ ∫ τ in t₀..t, ‖deriv c τ‖

--This is parameter transformation used to construct the arc-length reparametrization
def arclengthParamTransformFrom :=
  let ψ := revParamTransformForArclengthReparamFrom c t₀
  ψ⁻¹

--an arclength reparametrization of a parametrized curve
 def arclengthReparamFrom : ℝ → E :=
  let φ := arclengthParamTransformFrom c t₀
  c ∘ φ

[Michael Rothgang]

You should use letI inside your definitions. (Otherwise, your proof terms will be more complicated and your first step in using them will be to simplify them.)

[Michael Rothgang]

I'm not sure why there's a From in all your names: can you say why?

[Michael Rothgang]

Another option for definitions is to say arcLengthParamTransformAux - for "auxiliary definition". If you add a comment that they are auxiliary, that is not rare in mathlib.

[Michael Novak]

Michael Rothgang said:

You should use letI inside your definitions. (Otherwise, your proof terms will be more complicated and your first step in using them will be to simplify them.)

Thank you very much! I never heard of letI, it seems like a great idea, and also using Aux in the name is a great idea. The reason I have From in all the definitions is that it follows the naming @Sébastien Gouëzel suggested - they are constructed from c and t₀. Do you think I should avoid it?

[Michael Novak]

These are the updated definitions:

import Mathlib

noncomputable section

variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℝ → E) (t₀ : ℝ)

/-- Auxiliary definition, this is the reversed (inverse) parameter transformation
for the arclength reparametrization. -/
def revParamTransformForArclengthReparamAux : ℝ → ℝ :=
  fun t ↦ ∫ τ in t₀..t, ‖deriv c τ‖

--This is parameter transformation used to construct the arc-length reparametrization.
def arclengthParamTransformFrom :=
  letI ψ := revParamTransformForArclengthReparamAux c t₀
  ψ⁻¹

--Unit speed / arclength reparametrization of a parametrized curve
 def arclengthReparamFrom : ℝ → E :=
  letI φ := arclengthParamTransformFrom c t₀
  c ∘ φ

[Sébastien Gouëzel]

Once you have your definitions, the only way to see if they're good or if they're flawed is to start proving theorems about them. (I have the impression there are still issues, but it's more pedagogical if you discover them yourself while trying to prove theorems)

[Michael Novak]

Sébastien Gouëzel said:

Once you have your definitions, the only way to see if they're good or if they're flawed is to start proving theorems about them. (I have the impression there are still issues, but it's more pedagogical if you discover them yourself while trying to prove theorems)

O.k, I'll try to prove some theorems now and see how it goes. Thanks a lot!

[Michael Novak]

Is there some excepted way to create a short name (maybe ψ, for example) for the expressionrevParamTransformForArclengthReparamAux c t₀? I will be using it only in some auxiliary lemmas, but it looks a bit ridiculous having to type this long expression every time, especially in the statement of a lemma.

[Sébastien Gouëzel]

Does

local notation3 "ψ" => revParamTransformForArclengthReparamAux c t₀

work for you?

[Sébastien Gouëzel]

(Also, you can/should definitely use a shorter name!)

[Michael Novak]

Sébastien Gouëzel said:

Does

local notation3 "ψ" => revParamTransformForArclengthReparamAux c t₀

work for you?

It works great, thank you very much!

[Michael Novak]

Sébastien Gouëzel said:

(Also, you can/should definitely use a shorter name!)

You are absolutely right, but I don't know what is a good short description of it. Maybe I'll have some idea later.

[Michael Rothgang]

I was thinking of arclengthParamTransformAux, by the way.

[Michael Novak]

That's a good idea, it's definitely shorter. But is it still o.k., that I use the ψ notation (only on auxiliary lemmas) when I change it?

[Michael Novak]

I have this working code so far:

import Mathlib

open MeasureTheory intervalIntegral

/-- This is a version of the first part of FTC for a function which is continuous on an interval.
    Credit to Aaron Liu. -/
theorem derivWithin_integral_of_continuousOn_interval {I : Set ℝ} [I.OrdConnected] {f : ℝ → ℝ}
  (h : ContinuousOn f I) (x₀ x : I) : HasDerivWithinAt (fun t ↦  ∫ τ in x₀..t, f τ) (f x) I x :=
  have : intervalIntegral.FTCFilter x (nhdsWithin x I) (nhdsWithin x I) := by
    refine @intervalIntegral.FTCFilter.mk x (nhdsWithin x I) (nhdsWithin x I) ⟨?_⟩ ?_ ?_ ?_
    · rw [Filter.tendsto_smallSets_iff]
      intro t ht
      rw [mem_nhdsWithin_iff_exists_mem_nhds_inter] at ht
      obtain ⟨u, hu, hut⟩ := ht
      obtain ⟨a, b, haxb, habx, habu⟩ := exists_Icc_mem_subset_of_mem_nhds hu
      have hab : Set.Icc a b ∩ I ∈ nhdsWithin x.1 I :=
        Set.inter_comm _ _ ▸ inter_mem_nhdsWithin I habx
      filter_upwards [Filter.prod_mem_prod hab hab] with (i, j) ⟨hi, hj⟩
      refine subset_trans (Set.subset_inter ?_ ?_) hut
      · refine subset_trans ?_ habu
        intro k hk
        exact ⟨hi.1.1.trans hk.1.le, hk.2.trans hj.1.2⟩
      · intro k hk
        exact Set.Icc_subset I hi.2 hj.2 (Set.Ioc_subset_Icc_self hk)
    · exact pure_le_nhdsWithin x.2
    · exact nhdsWithin_le_nhds
    · exact @Filter.inf_isMeasurablyGenerated _ _ _ _ _
        (Set.OrdConnected.measurableSet ‹_›).principal_isMeasurablyGenerated
  intervalIntegral.integral_hasDerivWithinAt_right
    ((h.mono (Set.OrdConnected.uIcc_subset ‹_› x₀.2 x.2)).intervalIntegrable)
    (h.stronglyMeasurableAtFilter_nhdsWithin (Set.OrdConnected.measurableSet ‹_›) x)
    (h.continuousWithinAt x.2)

noncomputable section

variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℝ → E)

/-- Auxiliary definition, this is the reversed (inverse) parameter transformation
for the arclength reparametrization. -/
def arclengthParamTransformAux (t₀ : ℝ): ℝ → ℝ := fun t ↦ ∫ τ in t₀..t, ‖deriv c τ‖

--This is parameter transformation used to construct the arc-length reparametrization.
def arclengthParamTransform (t₀ : ℝ) :=
  letI ψ := arclengthParamTransformAux c t₀
  ψ⁻¹

--Unit speed / arclength reparametrization of a parametrized curve
def arclengthReparamFrom (t₀ : ℝ) : ℝ → E :=
  letI φ := arclengthParamTransform c t₀
  c ∘ φ

-- We now also assume c is a parametrized curve of class Cʳ from the interval I, r≥1.
variable (I : Set ℝ) [I.OrdConnected] (hI : IsOpen I) {r : WithTop ℕ∞}
  (once_diff : 1 ≤ r) (hc : ContDiffOn ℝ r c I) (t₀ : I)

--Auxilary definition, so we don't have to type the full long expression everytime
local notation3 "ψ" => arclengthParamTransformAux c t₀

/-- An auxiliary lemma giving us the derivitive of the reverse parameter transformation on I. -/
lemma rev_param_transform_deriv_eq_aux (t : I) (once_diff : 1 ≤ r) (hc : ContDiffOn ℝ r c I)
  (hI : IsOpen I) : HasDerivWithinAt ψ ‖deriv c t‖ I t := by
  have cont_speed : ContinuousOn (fun t ↦ ‖deriv c t‖) I :=
    Continuous.comp_continuousOn' continuous_norm (hc.continuousOn_deriv_of_isOpen hI once_diff)
  unfold arclengthParamTransformAux
  exact derivWithin_integral_of_continuousOn_interval cont_speed t₀ t

There are two issues that I wanted to ask about:
The first one is a bit weird - when I remove the assumptions once_diff, hc, hI from the statement of the last lemma, lean doesn't recognize these names inside the proof even though they already appear in the variable command above. Why is that? Is there some better way to do it which avoids repetition?
The second issue is about making a strategic decision about the use of intervals in the project. In the last lemma for example I assumed also that the interval I is open because I found a theorem on Mathlib that helped me get what I want which required I to be open. I might try to drop now the assumption that I is open and prove the lemma without it, but maybe it could be a good idea to just always assume that the interval is open to make life easier. Will that be acceptable if I want this code to eventually get into Mathlib? And do you think it will really be very helpful to assume the interval is open? Another option is to use a normal closed intervals as Michael Rothgang suggested previously, but it seems to me that this choice will still have the issue of dealing with edge points for which there isn't a neighborhood inside the interval.

[Aaron Liu]

The reason you need the interval to be open is you are using deriv, which looks at the neighborhood of whatever point you give it, and this neighborhood might go outside the interval if it is not open.

[Aaron Liu]

Michael Novak said:

The first one is a bit weird - when I remove the assumptions once_diff, hc, hI from the statement of the last lemma, lean doesn't recognize these names inside the proof even though they already appear in the variable command above. Why is that? Is there some better way to do it which avoids repetition?

This is because variables are not included into a theorem unless they are "relevant", messing appears in the statement or if a typeclass relating to a relevant variable. This is so that you don't accidentally change the statement of a theorem by messing around with its proof. You can get around it by doing include once_diff hc hI.

[Aaron Liu]

Surely you can get some derivative information from hc, so you don't have to use deriv?

[Michael Novak]

Aaron Liu said:

The reason you need the interval to be open is you are using deriv, which looks at the neighborhood of whatever point you give it, and this neighborhood might go outside the interval if it is not open.

Yes, I thought of using derivWithin, but then I will also need the original definition of arclengthParamTransformAux and the subsequent definitions to include the interval I, and I was told not to include it and also the theorem for the continuity of derivWithin require another assumption which is not completely clear to me, but if you think it's better to switch to derivWithin I'll look into it in more detail.

[Aaron Liu]

I don't think it should require another assumption

[Aaron Liu]

I'll take a look

[Aaron Liu]

oh it wants the derivative to be unique?

[Michael Novak]

Aaron Liu said:

I don't think it should require another assumption

The theorem I'm refering to is ContDiffOn.continuousOn_derivWithin, which also require this: (hs : UniqueDiffOn 𝕜 s₂). Do you think it's easy to show?

[Aaron Liu]

oh that why it wants the derivative to be unique

[Michael Novak]

Aaron Liu said:

oh it wants the derivative to be unique?

yes

[Aaron Liu]

I'll think about it

[Michael Novak]

Aaron Liu said:

Michael Novak said:

The first one is a bit weird - when I remove the assumptions once_diff, hc, hI from the statement of the last lemma, lean doesn't recognize these names inside the proof even though they already appear in the variable command above. Why is that? Is there some better way to do it which avoids repetition?

This is because variables are not included into a theorem unless they are "relevant", messing appears in the statement or if a typeclass relating to a relevant variable. This is so that you don't accidentally change the statement of a theorem by messing around with its proof. You can get around it by doing include once_diff hc hI.

I'm not sure I understand it completely. If these are assumptions about some variables like c and I which appear in the theorem statement, why are they not included?

[Aaron Liu]

They are not mentioned in the statement and they are not typeclass assumptions

[Michael Novak]

Why doesn't this HasDerivWithinAt ψ ‖deriv c t‖ I t count as a mention of c and I?

[Riccardo Brasca]

I didn't read everything, but mentioning I is not enough to have hI automatically included (it would work if the statement mention hI explicitly).

[Michael Novak]

Riccardo Brasca said:

I didn't read everything, but mentioning I is not enough to have hI automatically included (it would work if the statement mention hI explicitly).

Oh, that makes sense, thank you very much! And also thank you @Aaron Liu for trying to explain me that!

[Aaron Liu]

So the reason they want the derivative to be unique is that derivWithin picks out an arbitrary derivative and ContDiff only asserts the existence of a continuous derivative

[Aaron Liu]

so if the derivative isn't unique you can have the arbitrary derivative not the same as the continuous derivative

[Aaron Liu]

I claim you shouldn't be picking an arbitrary derivative with derivWithin and you should instead pick an arbitrary continuous derivative

[Michael Novak]

This sounds very weird to me. As far as I know the derivative is a limit and limits are unique. What do I miss?

[Aaron Liu]

for example, if your interval is a singleton point what's the derivative?

[Aaron Liu]

Michael Novak said:

As far as I know the derivative is a limit and limits are unique.

In mathlib a function f is said to have a derivative f' at x within a set s if f y - f x - f' * (y - x) as a function of y grows as little o of y - x at the neighborhood of x within s.

[Michael Novak]

I'm not sure, maybe it's not defined because there isn't an open subset (in the bigger normed space) of the point which is contained in the singleton. Now that I think of it, when I learned the general definition of the derivative of a multivariable function it was defined always when the domain of the function is an open set in the bigger normed space. Maybe Mathlib does something more general I'm not sure.

[Michael Rothgang]

Yes, that is what's happening: mathlib's definition docs#DifferentiableOn never requires the set to be open --- which is why considers docs#DifferentiableWithinAt. (For open sets, DifferentiableWithinAt and DifferentiableAt are equivalent.)

[Aaron Liu]

You can read docs#HasFDerivAtFilter

[Michael Novak]

Aaron Liu said:

Michael Novak said:

As far as I know the derivative is a limit and limits are unique.

In mathlib a function f is said to have a derivative f' at x within a set s if f y - f x - f' * (y - x) as a function of y grows as little o of y - x at the neighborhood of x within s.

I thought about it, it's a bit confusing, so I'm really not sure, but I think that according to this definition, the answer to your question about the case of a singleton is that any function f' would satisfy it vacuously (if we unfold the definition with epsilon and delta, then there isn't any point in any neighborhood of x without x itself within s). So if I understood this correctly I understand now the problem that the derivative could be not unique. But if we eliminate the case of a singleton is it still possible to get a non-unique derivative on an interval?

[Sébastien Gouëzel]

The singleton is the only problematic case. See docs#uniqueDiffOn_Icc and the lemmas around.

[Aaron Liu]

For a set of real numbera the derivative is always unique at non-isolated points

[Michael Novak]

So should I include an assumption that the interval I includes two different points and solve the issue in this way?

[Aaron Liu]

I think you should use something other than derivWithin that gets you a derivative which is automatically continuous

[Michael Novak]

Do you mean I should use docs#HasFDerivAtFilter ? If that's the best way to do it then I will try it. My main problem is that I barely understand what is a Filter (only read the definition in Wikipedia). Do you have a link for some information about using filters and related concepts in Mathlib?

[Aaron Liu]

not what I meant but I encourage you to learn about filters

[Michael Novak]

Could you elaborate what did you mean? (I will also try to lean about filters anyways :joy: ).

[Sébastien Gouëzel]

At a point x different from t0 you could use derivWithin (uIcc t0 x), and at t0 use deriv, for example.

[Aaron Liu]

ContDiffOn says there exists a sequence of multilinear maps whose first few terms form continuous derivatives for your given function within a certain set

[Aaron Liu]

so just take the derivative from there, and it's continuous by assumption

[Aaron Liu]

no need to use derivWithin that gives you a derivative not guaranteed to be continuous

[Michael Novak]

Thank you very much! I'll try this.

[Sébastien Gouëzel]

Aaron, inside intervals (different from a single point) the derivative is unique, and therefore continuous. The issue is not there. The issue is if you want something which works regardless of the interval I that you want to reparameterize.
@Michael Novak, thinking again about it, I think your life will be much easier if you allow yourself to let the reparam depend on the interval, or if you just take open intervals (in which case you can use the plain deriv). This really depends on the theorems you want to formalize, though.

[Michael Novak]

Sébastien Gouëzel said:

Aaron, inside intervals (different from a single point) the derivative is unique, and therefore continuous. The issue is not there. The issue is if you want something which works regardless of the interval I that you want to reparameterize.
Michael Novak, thinking again about it, I think your life will be much easier if you allow yourself to let the reparam depend on the interval, or if you just take open intervals (in which case you can use the plain deriv). This really depends on the theorems you want to formalize, though.

Your solution totally makes sense to me as well. The theorems I want to to formalize should work on any intervals, I'm not sure how much assuming the interval is open will help, certainly adding assumptions could not make life harder, but on the other hand as I understand it you want to be as general as you can in Mathlib, but I really don't have much experience with Mathlib as you, so I'm not sure. I'll wait to see what @Aaron Liu thinks.

[Michael Novak]

So I finished working on this theorem. I would really appreciate any feedback - what should I work on to make it suitable for the Mathlib library? There are two main issues: The first is that in the end I decided to assume that the interval is open, it made life much easier, but if you think this is very problematic and would not be acceptable on Mathlib, then I will try to generalize the work to any interval, although it might be a pain to do. The second one is about the statement of the main theorem: I couldn't think of a sensible way of splitting it to different theorems, if I was creating some structures, then for example the structure of a parameter transformation would come with an interval attached to it and this would make it much easier to split the theorem to multiple theorems. If you have any suggestion how reorganize the theorems I would love to know. And in general I would love to hear any feedback even about small style details.

I tried to paste the code here, but it's too long. So here is a link with the code:
https://paste.ofcode.org/E5wRc6yz4trHJKCRai7w5p

[Michael Novak]

I read a bit about contributing to Mathlib and I made a few small changes to the file to hopefully make better fit for Mathlib and I also read that it's better to make pull request to small pieces each time and find a reviewer. So I wanted to try to make a pull request for this file about arc-length reparametrization of parametrized curves, before I continue to prove more results about planar curves. So I was wondering if there's someone here that could be a reviewer for my code and also if someone here could help me with the technicalities of making a pull request, because I only recently created a Github account and I don't have any experience with it.
This is the current file:
ArcLengthReparametrization.lean

[Michael Rothgang]

Have you seen https://leanprover-community.github.io/contribute/index.html already? Does it answer your github-related questions?

[Michael Rothgang]

The arc length reparametrisation of curves sounds like a useful first step. I'm happy to review your PR (but very busy until mid-January - I cannot promise a response before then).

[Michael Rothgang]

In general, it seems clear enough that your code will find an interested reviewer: so you can open a PR before e.g. getting a review promise from a particular person. When opening my PRs, I just open the PR (and trust that there will be a reviewer) - rather than asking a particular reviewer in advance.

[Michael Novak]

Michael Rothgang said:

The arc length reparametrisation of curves sounds like a useful first step. I'm happy to review your PR (but very busy until mid-January - I cannot promise a response before then).

Thank you very much! Take your time, honestly I'm also very busy right now, so I have no problem waiting, and maybe there will also be someone else that would like to review as you said.

[Michael Novak]

Michael Rothgang said:

Have you seen https://leanprover-community.github.io/contribute/index.html already? Does it answer your github-related questions?

The first issue I have is that I don't know which option I should choose at the first step: "Choose different branches or forks above to discuss and review change"

[Michael Novak]

I don't think this is explained in the link you sent

[Michael Novak]

image.png

[Aaron Liu]

Have you pushed your changes to a branch of your fork yet?

[Michael Novak]

No, is that something that I need to do? And if so is there some guide on how to do it?

[Aaron Liu]

yes you do have to do it

[Aaron Liu]

it's in the thing Michael Rothgang linked

[Michael Novak]

Do you know in which section it is explained?

[Aaron Liu]

this section talks about how you make a fork and push to it

[Michael Novak]

Thank you very much!

[Michael Novak]

I work now on my fork now and I'm not sure where is the best place to put my file in. I was thinking maybe in Analysis/Calculus or maybe in Geometry/Manifold? And another question which might be silly - can I choose which license to use in my file (can I use the GNU GPL for example) or do all files have to use Apache?

[Ruben Van de Velde]

No, most definitely only Apache is allowed

[Michael Novak]

I created the PR now. Hopefully I didn't make too many mistakes :joy:

[Michael Novak]

It seems that I have some errors. Do you understand what's the problem?

[Kevin Buzzard]

Maybe post at least one of a link to the PR and the errors?

[Michael Novak]

https://github.com/leanprover-community/mathlib4/pull/33330

[Kevin Buzzard]

The error tells you what to do to fix it: run lake exe mk_all and then commit the new Mathlib.lean file which contains a mention of the new file you added

[Michael Novak]

So, just to make sure I understand, because I barely know how to use git: I first do this lake exe mk_all command inside the mathlib fork in my computer, then I do git add Mathlib.lean, then git commit and then git push and then do I need to do another PR in GitHub?

[Johan Commelin]

All of that sounds right, except you don't need to do another PR in GH after git push.

[Johan Commelin]

It will update your existing PR

[Yan Yablonovskiy 🇺🇦]

Michael Novak said:

So, just to make sure I understand, because I barely know how to use git: I first do this command inside the mathlib fork in my computer, then I do git commit and then git push and then do I need to do another PR in GitHub?

If you are working in the branch of the fork you are merging with mathlib (the PR) , then whatever you commit/push into that branch will be part of the merge PR.

i.e the changes you commit/push to the branch michael-novak-math:arclength-reparametrization-branch, will be reflected in the current PR you have .

[Michael Novak]

Thank you very much!

[Michael Novak]

I get this error when I try to do git push:
! [rejected] arclength-reparametrization-branch -> arclength-reparametrization-branch (fetch first) error: failed to push some refs to 'https://github.com/michael-novak-math/mathlib4.git' hint: Updates were rejected because the remote contains work that you do not hint: have locally. This is usually caused by another repository pushing to hint: the same ref. If you want to integrate the remote changes, use hint: 'git pull' before pushing again. hint: See the 'Note about fast-forwards' in 'git push --help' for details.

[Michael Novak]

I tried to follow the hints and somehow managed to push now. I hope the tests will work now.

[Michael Novak]

There's a new error in the PR now: https://github.com/leanprover-community/mathlib4/actions/runs/20536801096/job/58996064274. Could someone explain what's the problem?

[Ruben Van de Velde]

If you click on the little arrow next to "lint mathlib" and then on the coloured line with the :caution: icon, it should show actionable errors

[Ruben Van de Velde]

But you should see those as warnings in your editor locally as well

[Michael Rothgang]

In fact, the "build mathlib" step shows you the same errors (so I'd click on that instead, as it comes first).

[Michael Rothgang]

I left a comment explaining a bit more how to solve these. The second one ("cannot import non-modules inside modules") is indeed not beginner-friendly. I am sure that one will get better in one or two months. You should see the first one in your editor, and it should tell you mostly what to do.

[Michael Rothgang]

If you can't see those warnings in the editor, please ask here! (You don't want to miss out on that.)

[Michael Rothgang]

If you're not sure how to address them, similarly.

[Michael Rothgang]

I also left a few quick comments. I will return to it later (once you had a chance to address all comments), perhaps only in mid-January.

[Michael Novak]

Thank you very much, I'll look into that

[Michael Novak]

Sorry for the newbie question: if I made some changes (commits) to the branch in GitHub on the web browser, then how can I update the local fork on my computer?

[Kevin Buzzard]

You can just Google or ask an LLM for how to work git and GitHub, this is not lean specific and there are a ton of good resources. You can use git pull and git push to move commits between your local fork on your computer and GitHub.

[Michael Novak]

Sorry, I had a bit of an issue that git pull didn't work, but it was resolved, I wanted to delete the comment but there isn't such an option. I have now a different issue which I think is more related to lean: in the mathlib fork in my computer, every file that starts with mudule has this error:

unknown module prefix 'Mathlib'

No directory 'Mathlib' or file 'Mathlib.olean' in the search path entries:
/home/michael/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/lib/lean

[Ruben Van de Velde]

Huh, it definitely shouldn't do that!

[Michael Novak]

Also a different issue, that might be unrelated and just due to the fact that my computer is pretty bad or might be connected is that every time I tried to run lake build in the fork in my computer, my CPU gets to nearly 100% usage and after a minute or two my computer crash.

[Aaron Liu]

uhoh

[Aaron Liu]

did you lake exe cache get

[Michael Novak]

no, should I do it?

[Aaron Liu]

is lake build actually building things or is it just counting up to 7000

[Michael Novak]

how can I know?

[Aaron Liu]

it reportes the current file that it's working on

[Aaron Liu]

can you read the file name before it disappears

[Aaron Liu]

nvm

[Aaron Liu]

just run lake exe cache get

[Michael Novak]

o.k

[Aaron Liu]

it won't really do any harm even if it's unnecessary

[Michael Novak]

This was the output:

Current branch: arclength-reparametrization-branch
Using cache (Azure) from origin: michael-novak-math/mathlib4
Attempting to download 7794 file(s) from leanprover-community/mathlib4 cache
Downloaded: 7563 file(s) [attempted 7794/7794 = 100%, 75 KB/s]]
Attempting to download 231 file(s) from michael-novak-math/mathlib4 cache
Downloaded: 0 file(s) [attempted 231/231 = 100%, 1 KB/s]
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later.
Alternatively, if you already have pushed your commits to a branch, this may mean the CI build has failed part-way through building.
Decompressing 7563 file(s)
/home/michael/.cache/mathlib/86edffd46437e77c.ltar: removing corrupted file
/home/michael/.cache/mathlib/170d053d38e23641.ltar: removing corrupted file
/home/michael/.cache/mathlib/139738388054bd6b.ltar: removing corrupted file
/home/michael/.cache/mathlib/7b1ef49e559b72ee.ltar: removing corrupted file
/home/michael/.cache/mathlib/75f68ef6cf7cb2e1.ltar: removing corrupted file
/home/michael/.cache/mathlib/9d244000e72d4a57.ltar: removing corrupted file
/home/michael/.cache/mathlib/9fdca3b7ca56a861.ltar: removing corrupted file
/home/michael/.cache/mathlib/2edabac7ae2aad3e.ltar: removing corrupted file
/home/michael/.cache/mathlib/b893c179d26576fb.ltar: removing corrupted file
/home/michael/.cache/mathlib/42994fe1c2ba7f7f.ltar: removing corrupted file
/home/michael/.cache/mathlib/e36e90e403398a7a.ltar: removing corrupted file
/home/michael/.cache/mathlib/df43610ff397fdbc.ltar: removing corrupted file
/home/michael/.cache/mathlib/fb97058d81f0ea33.ltar: removing corrupted file
/home/michael/.cache/mathlib/c667a1fd6d47c342.ltar: removing corrupted file
/home/michael/.cache/mathlib/2d9d752dc84df6c2.ltar: removing corrupted file
/home/michael/.cache/mathlib/8cc3915510034709.ltar: removing corrupted file
/home/michael/.cache/mathlib/2faa083c35b04473.ltar: removing corrupted file
/home/michael/.cache/mathlib/efc8ad6a9e3dc11c.ltar: removing corrupted file
/home/michael/.cache/mathlib/9c33f8e3ac60c6f3.ltar: removing corrupted file
/home/michael/.cache/mathlib/5fab394be4b85953.ltar: removing corrupted file
/home/michael/.cache/mathlib/97c5c9596a34b84f.ltar: removing corrupted file
/home/michael/.cache/mathlib/2b9851e933dea3f7.ltar: removing corrupted file
/home/michael/.cache/mathlib/eea55a04deb43599.ltar: removing corrupted file
/home/michael/.cache/mathlib/c5cc97e6ea6fe4b7.ltar: removing corrupted file
/home/michael/.cache/mathlib/f45c2549b3137afc.ltar: removing corrupted file
/home/michael/.cache/mathlib/ff9b4fad0d83652b.ltar: removing corrupted file
/home/michael/.cache/mathlib/85c88e68cc5bf021.ltar: removing corrupted file
/home/michael/.cache/mathlib/c059373475063c11.ltar: removing corrupted file
/home/michael/.cache/mathlib/d5a759053a4e3806.ltar: removing corrupted file
/home/michael/.cache/mathlib/3def00a9e926294c.ltar: removing corrupted file
/home/michael/.cache/mathlib/34e5293a1821697f.ltar: removing corrupted file
/home/michael/.cache/mathlib/e6bd4fc21fc66007.ltar: removing corrupted file
/home/michael/.cache/mathlib/b2b7deac8f9375b8.ltar: removing corrupted file
/home/michael/.cache/mathlib/d807f1e04152b9ab.ltar: removing corrupted file
/home/michael/.cache/mathlib/a19641ad6e99999b.ltar: removing corrupted file
/home/michael/.cache/mathlib/cdedd14b4465f3a4.ltar: removing corrupted file
/home/michael/.cache/mathlib/36696acba7d0da4e.ltar: removing corrupted file
/home/michael/.cache/mathlib/3ccd3d1eec9a76b8.ltar: removing corrupted file
/home/michael/.cache/mathlib/18ba69dca29f31a1.ltar: removing corrupted file
/home/michael/.cache/mathlib/1eccb9bec3829a40.ltar: removing corrupted file
/home/michael/.cache/mathlib/b5807fb076ddeb8b.ltar: removing corrupted file
/home/michael/.cache/mathlib/422c50ba01a33cf0.ltar: removing corrupted file
/home/michael/.cache/mathlib/341351784cf06f45.ltar: removing corrupted file
/home/michael/.cache/mathlib/11a2789f521a380c.ltar: removing corrupted file
/home/michael/.cache/mathlib/cc15ff521b3c30a5.ltar: removing corrupted file
/home/michael/.cache/mathlib/7ba647abddbd8d0a.ltar: removing corrupted file
/home/michael/.cache/mathlib/db6c23dd2e59a69b.ltar: removing corrupted file
/home/michael/.cache/mathlib/28e7309dea9a5a27.ltar: removing corrupted file
/home/michael/.cache/mathlib/ec12b715e2b06634.ltar: removing corrupted file
/home/michael/.cache/mathlib/1143c749d3608aaf.ltar: removing corrupted file
/home/michael/.cache/mathlib/a5bdd54c7af6587b.ltar: removing corrupted file
/home/michael/.cache/mathlib/5992b30c5ebb8719.ltar: removing corrupted file
/home/michael/.cache/mathlib/fd3444b0e2051796.ltar: removing corrupted file
/home/michael/.cache/mathlib/77d727c1e0ded21f.ltar: removing corrupted file
/home/michael/.cache/mathlib/350a1f8d0293f929.ltar: removing corrupted file
/home/michael/.cache/mathlib/ba21b5298072ccec.ltar: removing corrupted file
Unpacked in 35110 ms
Completed successfully!

[Aaron Liu]

well it looks like something happened

[Aaron Liu]

now does lake build work?

[Michael Novak]

Should I try it again? And if so, should I stop it if I see that my CPU usage gets very high to prevent my computer from crashing again or just let it continue?

[Aaron Liu]

do try it again

[Michael Novak]

Btw, the message about module still exists

[Aaron Liu]

uhoh

[Michael Novak]

Aaron Liu said:

do try it again

O.k

[Aaron Liu]

I think of you don't want it to crash your computer then that's fine

[Aaron Liu]

is your PR #33330

[Michael Novak]

I tried it again but stopped in the middle to prevent a computer crash because the CPU was getting to 90%. This was the output:

[michael@libre-d16-desktop mathlib4]$ lake build
⚠ [1393/5859] Built Mathlib.Algebra.Order.PUnit
warning: /home/michael/documents/mathematics/lean-projects/mathlib4/.lake/build/lib/lean/Mathlib/Algebra/Order/PUnit.trace: offset 0: unexpected end of input
⚠ [1399/6113] Built Mathlib.Deprecated.RingHom
warning: /home/michael/documents/mathematics/lean-projects/mathlib4/.lake/build/lib/lean/Mathlib/Deprecated/RingHom.trace: offset 0: unexpected end of input
⚠ [1419/6113] Built Mathlib.Data.Int.Range
warning: /home/michael/documents/mathematics/lean-projects/mathlib4/.lake/build/lib/lean/Mathlib/Data/Int/Range.trace: offset 0: unexpected end of input
⣾ [1427/6113] Running Mathlib.Combinatorics.Quiver.Path.Vertices (+ 32 more)^C

[Michael Novak]

Aaron Liu said:

is your PR #33330

yes

[Aaron Liu]

I guess I don't really know what to do now

[Aaron Liu]

I'm not sure if going up to a high CPU usage is normal or not

[Michael Novak]

do you think that the module error is related to the lake build issue?

[Aaron Liu]

probably not?

[Aaron Liu]

that one is relatively easy to fix

[Michael Novak]

Because the module issue is the one that most practically bothering me now from trying to fix some things in the PR.

[Aaron Liu]

what's the error you're getting?

[Aaron Liu]

looking at your PR I don't think you should get this kind of error so the fix may be just a git pull

[Michael Novak]

In the mathlib fork in my computer, every file that starts with mudule has this error:

unknown module prefix 'Mathlib'

No directory 'Mathlib' or file 'Mathlib.olean' in the search path entries:
/home/michael/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/lib/lean

[Aaron Liu]

oh that's

[Michael Novak]

Aaron Liu said:

looking at your PR I don't think you should get this kind of error so the fix may be just a git pull

I already did it and if I do it again I just get the message Already up to date.

[Aaron Liu]

that's not the error I thought you had

[Aaron Liu]

Michael Novak said:

In the mathlib fork in my computer, every file that starts with mudule has this error:

unknown module prefix 'Mathlib'

No directory 'Mathlib' or file 'Mathlib.olean' in the search path entries:
/home/michael/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/lib/lean

is that just every file or are there files you don't get this error on

[Aaron Liu]

also, does it list only that one search path entry?

[Michael Novak]

I didn't check every file, but on the few files that I did check, they all had this error, so I believe they all have it, but can't tell for sure.

[Michael Novak]

Aaron Liu said:

also, does it list only that one search path entry?

yes

[Aaron Liu]

maybe try deleting your mathlib4/.lake folder?

[Aaron Liu]

and then run lake exe cache get again

[Michael Novak]

o.k, I'll try it, thanks

[Aaron Liu]

if this doesn't work then I'm out of ideas

[Michael Novak]

This is the output:

[michael@libre-d16-desktop mathlib4]$ lake update
info: toolchain not updated; already up-to-date
info: mathlib: running post-update hooks
[michael@libre-d16-desktop mathlib4]$ git pull
Already up to date.
[michael@libre-d16-desktop mathlib4]$ ranger
[michael@libre-d16-desktop mathlib4]$ lake exe cache get
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision 'b3dd6c3ebc0a71685e86bea9223be39ea4c299fb'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '5ce7f0a355f522a952a3d678d696bd563bb4fd28'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision 'cff9dd30f2c161b9efd7c657cafed1f967645890'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision 'ef8377f31b5535430b6753a974d685b0019d0681'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision 'fa78cf032194308a950a264ed87b422a2a7c1c6c'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '8920dcbb96a4e8bf641fc399ac9c0888e4a6be72'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '2e16f91af2a97975e5d2fac906494cd6c17ba255'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '726b98c53e2da249c1de768fbbbb5e67bc9cef60'
Fetching ProofWidgets cloud release... done!
Current branch: arclength-reparametrization-branch
Using cache (Azure) from origin: michael-novak-math/mathlib4
Attempting to download 287 file(s) from leanprover-community/mathlib4 cache
Downloaded: 56 file(s) [attempted 287/287 = 100%, 1 KB/s]]
Attempting to download 231 file(s) from michael-novak-math/mathlib4 cache
Downloaded: 0 file(s) [attempted 231/231 = 100%, 1 KB/s]
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later.
Alternatively, if you already have pushed your commits to a branch, this may mean the CI build has failed part-way through building.
Decompressing 7563 file(s)
Unpacked in 41155 ms
Completed successfully!

[Aaron Liu]

did it fix the problem

[Michael Novak]

It didn't fix the module error

[Aaron Liu]

what if you restart Lean?

[Michael Novak]

how can I do this?

[Aaron Liu]

you are using VSCode?

[Aaron Liu]

click on the search bar at the very top and type >restart server

[Aaron Liu]

and pick the option that restarts the lean4 server

[Michael Novak]

Aaron Liu said:

you are using VSCode?

typically I used nvim, but now when I use nvim on this fork my computer also crash after a minute or two, although I didn't check this in the last hour or two so maybe it changed. So now I use codium (basically VSCode) and this is where is see the module error, but at least there are no crashes.

[Aaron Liu]

oh

[Michael Novak]

Aaron Liu said:

click on the search bar at the very top and type >restart server

O.k

[Michael Novak]

It didn't make a difference. I also closed the editor and reopened again, but still the same error.

[Aaron Liu]

then I'm really out of ideas

[Michael Novak]

O.K, I have no idea what happened, maybe the gods wanted to help us, but some how when I tried now to open the files in nvim, there isn't any module errors :joy: Thank you very much for your help!