v4.10.0 discussion

Stream: general

[Bulhwi Cha]

Char.csize is replaced by Char.utf8Size (#4357).

There are still some theorems in Batteries.Data.String.Lemmas whose name contains csize. I'll make a pull request that renames these theorems.

[Bulhwi Cha]

When I right-click Char.utf8Size and try to go to its definition in VS Code, the Lean server responds that no definition is found for it.

[Bulhwi Cha]

Bulhwi Cha said:

There are still some theorems in Batteries.Data.String.Lemmas whose name contains csize. I'll make a pull request that renames these theorems.

@Kim Morrison Here's my PR: std#901.

[Max Nowak 🐉]

I am very happy about the customizable #reduce! This update is great ^^

[Yury G. Kudryashov]

About List.get vs l[n]. Am I right that l[n] is in fact l[n]'[hn], so in some sense we're going back from List.get l (n : Fin l.length) to docs#List.nthLe with a new name/syntax? How do we call l[n] in lemma names?

[Eric Wieser]

getElem is the name for the syntax

[Yury G. Kudryashov]

Do, do we restore nthLe lemmas with getElem names&syntax now and deprecate List.get?

[Kim Morrison]

I think if there are useful deprecated lemmas with nthLe in their name, yes, it would be good to turn them into lemmas about getElem. I don't think we should systematically try to recover unused, deprecated lemmas.

[Yury G. Kudryashov]

This will happen automatically as we migrate from List.get to getElem.

[Eric Wieser]

Is .get going away, or should we keep around lemmas about it?

[Eric Wieser]

I'd argue we want to keep it, to act as an inverse to List.ofFn

[Yury G. Kudryashov]

We can use fun i : Fin l.length => l[i]

[François G. Dorais]

List.nthLe is obsolete and must be deprecated in favor of [*] notation. When using [*] notation, theorem names should say getElem and not get.

List.get (which is in Init.Prelude) is not deprecated but it is low-level. Only a few theorems do need to use get explicitly instead of getElem, these theorem names should still use get where they do.

[Kim Morrison]

get is staying around in core Lean. The "programming API" for Lean will treat it as low-level, and uniformly prefer getElem.

That said, in combinatorial applications there are places where indexing over Fin really makes more sense, and then get is more ergonomic in some statements. My preference is that these places continue to use get, but resist the temptation to (re)build massive parallel API, and instead try to conduct most proofs by simplifying get back to getElem and using the API there.

[Kim Morrison]

(I think this is agreeing with @François G. Dorais above!)

[François G. Dorais]

Indeed, I think we agree. To emphasize/rephrase in a very informal manner: Lean "noobs" should only encounter [*] notation and use getElem theorems, unless they find themselves drowning in a situation they shouldn't be in to start with.

[François G. Dorais]

@Kim Morrison But if i : Fin a.size then a[i] is just a.get i so the applications you're thinking of just need a better get_elem_tactic (and perhaps other bells and whistles).

[Yury G. Kudryashov]

I'm going to try to cleanup Mathlib (get/getElem/nthLe) over the weekend (see #15455 for the current draft).

[Yury G. Kudryashov]

What should we do about docs#Fin.instGetElemFinVal ?

[Yury G. Kudryashov]

Special case each lemma for Fin?

[Yury G. Kudryashov]

simp to Nat?

[Yury G. Kudryashov]

Never mind, we already simp to Nat. I was debugging a simp only call.

[Yury G. Kudryashov]

I should've read 10 lines around the instance before posting here.

[Dan Velleman]

The following worked in v4.8.0, but in v4.10.0, rfl fails. Anyone know why?

def gcd (a b : Nat) : Nat :=
  match b with
    | 0 => a
    | n + 1 =>
      have : a % (n + 1) < n + 1 := Nat.mod_lt a (Nat.succ_pos n)
      gcd (n + 1) (a % (n + 1))
  termination_by b

example (a : Nat) : gcd a 0 = a := by rfl

[Matthew Ballard]

unseal gcd in
example (a : Nat) : gcd a 0 = a := rfl

is one way to do it now.

[Dan Velleman]

What does unseal mean? Has rfl been changed so that it no longer looks at the definition of gcd?

[Matthew Ballard]

The attributes of gcd have changed so that rfl doesn't automatically unfold it

[Matthew Ballard]

Functionally, unseal foo is equivalent to attribute [local semireducible] foo.

[Dan Velleman]

Note that I am using my own gcd function, not a built-in function (perhaps it should be called my_gcd). What is it about my definition of my gcd function that causes rfl not to unfold it?

[Marcus Rossel]

Dan Velleman said:

What is it about my definition of my gcd function that causes rfl not to unfold it?

This is explained in the Lean v4.9.0 release blog post:

Functions defined by well-founded recursion are now irreducible by default. This eliminates performance gotchas [...]

For such definitions, it's usually much better to explicitly rewrite using the equational lemmas that Lean generates, and the simplifier does this whenever the definition's name is specified as a simp rule. In Lean 4.9, these definitions are irreducible, which means that Lean will not unfold them unless explicitly asked to and the proofs no longer slow down computation.

[Edward van de Meent]

tldr: the fact that it is defined with WF-flavour recursion

[Kyle Miller]

Here's how you can permanently unseal it:

@[semireducible] def gcd (a b : Nat) : Nat :=
  match b with
    | 0 => a
    | n + 1 =>
      have : a % (n + 1) < n + 1 := Nat.mod_lt a (Nat.succ_pos n)
      gcd (n + 1) (a % (n + 1))
  termination_by b

example (a : Nat) : gcd a 0 = a := by rfl

[Dan Velleman]

Thanks. For my purposes, that may be the best option.

[Dan Velleman]

One more small issue. I am in the habit of using done at the end of a tactic proof. That now generates a warning, with the suggestion that set_option linter.unusedTactic false will suppress the warning. That works, but I tried putting moreGlobalServerArgs = ["-Dlinter.unusedTactic=false"] in my lakefile.toml, and that doesn't work--Lean complains that linter.unusedTactic is an unknown configuration option. Why?

[Kyle Miller]

It looks like @Damiano Testa included a way to make a blanket exception for a particular tactic.

#allow_unused_tactic Lean.Parser.Tactic.done

[Dan Velleman]

But is there a way to put something in my lakefile.toml that will fix the problem in all files in the project, rather than having to put a command at the top of every file?

[Kyle Miller]

That's as far as I got looking into it, I'll leave it to @Damiano Testa. I was thinking that you could potentially add it into a library file that everything else includes, but I don't know if it persists from one module to another.

[Dan Velleman]

I was surprised that an option that works in set_option was not recognized when used in moreGlobalServerArgs.

[Kyle Miller]

Oh right, linter.unusedTactic is defined within mathlib, so it can't be set from the command line — until a recent version of Lean that is. It might be -Dweak.linter.unusedTactic=false, but I don't remember if mathlib currently is using the Lean with this feature. Edit: It looks like it is available on the master branch, but it's not in the 4.10.0 release.

[Dan Velleman]

So it will be available in 4.11.0?

[Kyle Miller]

Yes

[Damiano Testa]

There is #15616 that systematically uses the new "option framework" in mathlib.

[Damiano Testa]

I do not remember if the fix for excluding tactic from the unusedTactic linter would persist beyond the file with the exclusion: I hope that it would, but I am not sure that it has actually been tested.

[Damiano Testa]

I just did a quick experiment, and it seems that #allow_unused_tactic does not persist. With a current version of mathlib, you should be able to disable completely the unusedTactic linter, but I would have to think of an alternative solution to make the linter active, and yet have exceptions persist in imported files.

[Damiano Testa]

Btw, when I teach, I also tell my students to start with a proof template by sorry; done. I also like the linter to warn about unused tactics, so I would like to have a better solution to this issue.

[François G. Dorais]

Dan Velleman said:

So it will be available in 4.11.0?

It is already in v4.11.0-rc1.

[Dan Velleman]

Well, I updated to v4.11.0-rc1 and I now no longer get an error message when I include "-Dweak.linter.unusedTactic=false" in moreGlobalServerArgs. However, I still get the warning that done does nothing, so it doesn't seem to be setting the option. Any ideas?

[Dan Velleman]

"-Dlinter.unusedTactic=false" doesn't work either.

[Damiano Testa]

I do not know from the command-line, but the PR above sets the lake-file. The lakeOptions have weak and are relevant for lake build, while moreServerArgs (I think that the docs say something else, but this should be correct) set the options that you see highlighted in VSCode.

[Dan Velleman]

Yes, that's what I thought. So I thought that with moreGlobalServerArgs = ["-Dlinter.unusedTactic=false"] I would not see the warnings about done in VS Code. But I still see the warnings.

[Dan Velleman]

After a little more experimentation, I think using moreServerOptions works, but moreServerArgs doesn't. Is the issue that moreServerArgs is applied at the command line, and (as @Kyle Miller commented earlier) this option can't be set at the command line?
Now my problem is that I really wanted to use moreGlobalServerArgs, but there's no moreGlobalServerOptions, is there?

[François G. Dorais]

I'm pretty sure moreGlobalServerArgs and moreServerArgs are synonyms and the latter is deprecated. I don't understand why moreServerOptions is not sufficient to suppress all the warnings you care about? Where do you see undesired warnings?

[Mario Carneiro]

it sounds to me like moreServerOptions := #[⟨`linter.unusedTactic, false⟩] is what you want

[Dan Velleman]

As I understand it, moreServerArgs applies to all files that are in targets of the package, but moreGlobalServerArgs applies to all files that you open in VS Code, even if they are not in targets of the package. My default target is a library, but I have some files that are not part of that library. Those files contain exercises for students to do. The student is supposed to prove some theorems in those files, but I don't see any reason for those files to ever get built, so I didn't put them in a target. (In fact, a few exercises are incorrect theorems--the student is supposed to try to prove them and see where they get stuck.) Arguments in moreServerArgs don't get applied to the student exercise files, but those in moreGlobalServerArgs do.
I'm not sure what the recommended configuration for this package is. Perhaps I'm supposed to define a second target, put the student exercise files in that target, and then never build that target?

[François G. Dorais]

Does setting weakLeanArgs := #["-Dweak.linter.unusedTactic=false"] work? (The two "weak" mean different things!)

[François G. Dorais]

Dan Velleman said:

I'm not sure what the recommended configuration for this package is. Perhaps I'm supposed to define a second target, put the student exercise files in that target, and then never build that target?

That's probably the best option. lake doesn't know what to do with files that aren't in a target.

[Mario Carneiro]

My default target is a library, but I have some files that are not part of that library. Those files contain exercises for students to do. The student is supposed to prove some theorems in those files, but I don't see any reason for those files to ever get built, so I didn't put them in a target.

If you don't want a target to get built by default, just don't put @[default_target] on the library. I think this is probably better than just having them as loose files because then lake can apply settings to them and know how they fit into the project layout

[Dan Velleman]

Thanks. That seems to do what I want.

[Damiano Testa]

Does this mean that Archive and Counterexamples should be marked as @[default_target], so that the linters act on them as they do on Mathlib itself?

[François G. Dorais]

No, they just need to be targets.

[Damiano Testa]

In the context of #15616, Archive and Counterexamples are not linted by the Mathlib linters: how do I make them targets?

[François G. Dorais]

They're already targets but the linter doesn't know about them.

[François G. Dorais]

The linter needs an update.

[François G. Dorais]

Actually, this is complicated. I have no idea why the Mathlib linter even works at all. Certainly, the makefile only runs it on Mathlib but is it still run through make?