Lean 3.15.0

Stream: general

[Gabriel Ebner]

Good evening, mathematicians and computer scientists! May I announce the sixth release of the Lean community fork this month, Lean 3.15.0! Many thanks to @Edward Ayers and @Bryan Gin-ge Chen for their contributions! Let me show you the excerpt from the changelog!

Features:

• Support for structured formatting using eformat (lean#276)
• Show goals for subterms (lean#275, lean#277)
• Freeze instances in the simplifier (lean#273)
• Support local attribute with docstring (lean#271)
• VM objects may be hashed (lean#262)
• expr.coord and expr.address (lean#260)
• Add list.map_with_index to core library (lean#259)
• Add expr.instantiate_vars_core (lean#261)
• Don't check levels on meta inductives (lean#263)

Bug fixes:

• Preserve VM code indexes across instances (lean#283)
• Fixes a VM environment cache not updating (lean#280)
• Do not use fseek in io.fs.read (lean#278)
• Dot-notation pretty-printing (lean#269)

Changes:

• Elaborate structure instances left-to-right (lean#282)
• Remove duplicated namespaces (lean#267)
• Remove (| and |) aliases (lean#265)

Special feature: widgets (lean#258)

Lean API

• Add widgets. This is an HTML-based UI framework for generating html within lean to enable interactive UI
  in the infoview in vscode and on the web.

• Add tactic.save_widget: pos → widget.component tactic_state string → tactic unit. Examples of widgets can be found in library/widget/examples.lean.
  Widgets are registered in exactly the same way as save_info_thunk saves text.

• Use the #html command to view html empty or component tactic_state string widgets.

• Add a 'structured format' pretty printing system tactic_state.pp_tagged : tactic_state → expr → eformat.
  eformat := tagged_format (expr.address × expr).
  tagged_format α : Type performs the same role as format except that there is a special constructor
  tag : α → tagged_format → tagged_format that contains information about
  which subexpression caused this string to be rendered.
  This is used to implement a widget which allows the user to hover over a pretty printed string
  and view information about the subexpressions that build up the original expression.
  For example, this lets you view types of pretty printed expressions and view implicit arguments.

• Add numerous docstrings

[Gabriel Ebner]

The mathlib PR is building : #2851 (feel free to fix things)

[Bryan Gin-ge Chen]

@Edward Ayers The widgets feature for vscode-lean is still WIP, right? I'd be happy to review a PR for this feature to the community web editor whenever you're ready.

[Edward Ayers]

It’s all wip but hopefully it will drop on vscode soon

[Mario Carneiro]

Wow, six releases in one month. Should we perhaps use more minor versions just to keep the version numbers under control?

[Mario Carneiro]

or maybe we need relative numbering like 3.mathlib.0 and 3.mathlib+1.0

[Bryan Gin-ge Chen]

I think the current versioning scheme paints a good picture of the rate of development.

[Patrick Massot]

Edward Ayers said:

It’s all wip but hopefully it will drop on vscode soon

Where's that cheerleader emoji?

[Bryan Gin-ge Chen]

Any more thoughts on #2851 ? Since there were quite a few changes necessary, I think it would be good to have more eyes on it before merging.

[Johan Commelin]

I didn't contribute to the PR, but I can try to review

[Kevin Buzzard]

I just looked at it and it's the most random PR I've ever seen

[Johan Commelin]

I don't have further comments. Let's get this merged.

[Bryan Gin-ge Chen]

It's now in the merge queue, but the last batch failed to build, so there might be an incompatibility with one of the other PRs (#2861, #2870 or #2876): https://github.com/leanprover-community/mathlib/runs/723943411?check_suite_focus=true#step:7:11

[Bryan Gin-ge Chen]

OK, the culprit seems to be #2861 (see comment there).

[Chris Hughes]

I downloaded the branch, and it works fine on my computer.

[Bryan Gin-ge Chen]

Yeah, I now think the issue is with #2851 and something that was already merged.

[Chris Hughes]

#2848 seems the most likely culprit

[Chris Hughes]

Is there a way to download the incomplete set of oleans?

[Bryan Gin-ge Chen]

The oleans should be on azure, but it might be a pain to get to the exact commit. I've just pushed a merge commit so in ~1 hour there should be some olean files for a broken build on the 315 branch.

[Bryan Gin-ge Chen]

Hmm, 315 builds on my computer (without -T100000).

[Bryan Gin-ge Chen]

The timeout with -T100000 is here under the ≃ₗ.

[Bryan Gin-ge Chen]

No deterministic timeout if I change it from this:

def eval_equiv (h : dim K V < omega) : V ≃ₗ[K] dual K (dual K V) :=
linear_equiv.of_bijective (eval K V) eval_ker (eval_range h) -- deterministic timeout

to this:

def eval_equiv (h : dim K V < omega) : V ≃ₗ[K] dual K (dual K V) :=
linear_equiv.of_bijective (eval K V) eval_ker (@eval_range _ _ _ _ _ h) -- slow, but succeeds

[Chris Hughes]

I think it might be because of some bad instances where one := 1 etc. was not used like recommended

[Chris Hughes]

Building locally to test this hypothesis.

[Bryan Gin-ge Chen]

The github actions build failed, so you should be able to get partial oleans now.

[Chris Hughes]

Deleting dual.vector_space seemed to make the difference.

[Chris Hughes]

The instances generated by extends don't follow Gabriel's advice. Is this a problem?

Avoid sourcing ({ ..e } where e.g. e : euclidean_domain α) for fields like add, mul, zero, etc. Instead write { add := (+), mul := (*), zero := 0, ..e }. The reason is that { ..e } is equivalent to { mul := euclidean_domain.mul, ..e }. And euclidean_domain.mul should never be mentioned.

[Chris Hughes]

It builds

[Reid Barton]

Generally, these new guidelines seem unintuitive and easy to forget. Is there some way a linter could help?