No notation in #docs

Stream: mathlib4

[Yaël Dillies]

It looks like the docs currently have absolutely no notation in them! :scream: eg docs#add_zero looks like Eq (HAdd.hAdd a 0) a to me right now.

[Rémy Degenne]

Look at this: ProbabilityTheory.HasSubgaussianMGF.measure_sum_range_ge_le_of_iIndepFun
The Mathlib docs are full of HMul.hMul instead of simply *. Same for all other operations, and we get things like this:

LE.le (DFunLike.coe μ (setOf fun (ω : Ω) => LE.le ε ((Finset.range n).sum fun (i : Nat) => X i ω))).toReal
  (Real.exp (HDiv.hDiv (Neg.neg (HPow.hPow ε 2)) (HMul.hMul (HMul.hMul 2 n.cast) c.toReal)))

instead of

(μ {ω | ε ≤ ∑ i ∈ Finset.range n, X i ω}).toReal ≤ exp (- ε ^ 2 / (2 * n * c))

[Yaël Dillies]

@Kim Morrison, is this related to the v4.19.0-rc2 bump by any chance?

[Henrik Böving]

@Kyle Miller are there recent changes to the pretty printer that could affect doc-gen here?

[Kevin Buzzard]

IIRC when I was deciding between theorem provers years ago I found that some of the other communities regarded notation with suspicion (especially unicode notation!) because "it obscured what was really going on and had no real benefit" or something. Maybe we're trying this idea ourselves now? :-)

[Kevin Cheung]

I am seeing at https://leanprover-community.github.io/mathlib4_docs/Init/Data/Nat/Lemmas.html#Nat.mul_eq_zero the following:

theorem Nat.mul_eq_zero {m n : Nat} :
Iff (Eq (HMul.hMul n m) 0) (Or (Eq n 0) (Eq m 0))

I remember seeing it in the past as

theorem Nat.mul_eq_zero {m n : Nat} :
 n * m = 0 ↔ n = 0 ∨ m = 0

Does the documentation no longer use notation for Iff, Or, HMul etc.?

[Yaël Dillies]

See #mathlib4 > No notation in #docs

[Kevin Cheung]

Thanks.

[Floris van Doorn]

Note: as a workaround, people can temporarily use
https://florisvandoorn.com/carleson/docs/
(or the docs from any other repo).
That uses Mathlib from yesterday (and Lean v4.18.0)

[Kim Morrison]

Looks like a bug, presumably a problem in doc-gen4 after the upgrade. I noticed the same problem in lean4checker actually, and should have been more suspicious about it being a widespread problem.

[Kim Morrison]

I think this must be a consequence of lean#6325 somehow.

[Kim Morrison]

My wild guess is that

def envOfImports (imports : Array Name) : IO Environment := do
  -- needed for modules which use syntax registered with `initialize add_parser_alias ..`
  unsafe Lean.enableInitializersExecution
  importModules (imports.map (Import.mk · false)) Options.empty (leakEnv := true)

in doc-gen4 needs a (loadExts := true) at the end.

[Kim Morrison]

I would like there to be some test in doc-gen4 CI that detects this issue!

[Kim Morrison]

I guess we don't have any test there that actually inspects the output closely enough...

[Eric Wieser]

Kim Morrison said:

in doc-gen4 needs a (loadExts := true) at the end.

I guess a corollary here is that if you want to load an environment and pretty-print from it, then you need to load extensions?

[Kim Morrison]

I'm out of time to investigate tonight, but if someone could try to reproduce the problem locally in doc-gen4, and then try that fix?

[Edward van de Meent]

Floris van Doorn said:

Note: as a workaround, people can temporarily use
https://florisvandoorn.com/carleson/docs/
(or the docs from any other repo).
That uses Mathlib from yesterday (and Lean v4.18.0)

do note that this only shows the parts of mathlib that the project uses!

[Edward van de Meent]

e.g. things like docs#Partrec don't show up

[Henrik Böving]

Kim Morrison said:

My wild guess is that

def envOfImports (imports : Array Name) : IO Environment := do
  -- needed for modules which use syntax registered with `initialize add_parser_alias ..`
  unsafe Lean.enableInitializersExecution
  importModules (imports.map (Import.mk · false)) Options.empty (leakEnv := true)

in doc-gen4 needs a (loadExts := true) at the end.

Oh I did have this on my radar but this was merged after 4.19 wasn't it? Or did you backport that change?

[Henrik Böving]

I'm surprised anything works at all in doc-gen without loading the extensions, I would've expected it to crash hard

[Jovan Gerbscheid]

Also, any class now shows up as a structure in the docs

[Henrik Böving]

That's all caused by the same effect

[Henrik Böving]

Will be fixed in 15

[Henrik Böving]

fixed

[Jannis Limperg]

I think this is a good illustration of the dangers of default arguments: they tend to break code without compilation errors. That also makes them convenient (and probably as a result, core is very fond of them), but I just want to flag the tradeoff in case it hasn't been considered yet.

[Henrik Böving]

In this situation by just setting the default to true we would've maintained full backwards compatability so I think in this situation it's not the default arguments themselves but the value that we choose.

[Jannis Limperg]

Even then, I'd prefer it to be a non-default argument. As a downstream user, this alerts me to a potentially relevant change, in this case a potential optimisation opportunity.

Although I guess the tradeoff is different if you're maintaining a project that seeks to be compatible with multiple Lean versions, e.g. Subverso. Then you'd appreciate maximum compatibility.

[Kim Morrison]

Apologies here. I initially didn't include lean#6325 in v4.19.0-rc1 precisely because I was worried about the possibility of problems like this. Then I realised that there was going to be no way to get lean4checker running on v4.19.0-rc1, and somewhat hurriedly backported it into v4.19.0-rc2, and stepped on this landmine...

[Kim Morrison]

Happily because of the slightly indirect dependency structure for doc-gen4, we don't actually need to retag any of the v4.19.0-rc2 tags of the repositories.

[Kim Morrison]

@Henrik Böving, is there something that we could add to doc-gen4 CI so I would have seen this problem before merging the mistake?

[Notification Bot]

4 messages were moved from this topic to #general > docgen scoped notations by Kyle Miller.

[Henrik Böving]

Kim Morrison said:

Henrik Böving, is there something that we could add to doc-gen4 CI so I would have seen this problem before merging the mistake?

We can in principle run a full integration test and assert that the produced HTML is of some shape I guess? Though I'm not sure how beneficial that is in the long run