autoImplicits

Stream: lean4

[Kevin Buzzard]

I am trying to understand the FLT project's lakefile so I can document it. It currently starts like this:

def moreServerArgs := #[
  "-Dpp.unicode.fun=true", -- pretty-prints `fun a ↦ b`
  "-Dpp.proofs.withType=false", -- no idea what this does
  "-DautoImplicit=false", -- attempt to switch off auto-implicit
  "-DrelaxedAutoImplicit=false" -- attempt to switch off relaxed auto-implicit
]

The reason I have autoimplicits set to max off is that I personally am a rubbish coder. I am constantly making typos/misspellings and I really need Lean to say "no you goofed up here Kevin". But I am wondering whether this is a particularly good reason to enforce this convention on my coworkers. In my dream world I would just have a switch somewhere in VS Code in the upside-down A saying "switch on autoimplicits", which I'd do if I was writing my own code, and if I was looking at Lean code with this switch off then some window in VS Code would be shaded slightly red or something :-).

Another example where I'd like to play with autoImplicits is when I have mathlib open and someone posts a question on the Zulip which doesn't involve mathlib and where autoimplicits are on by default so are not mentioned in the MWE, which then doesn't work for me locally in a scratch file. I'd like to just switch them on quickly when trying to answer the question and then switch them back off.

[Yury G. Kudryashov]

You can turn it on in a single file.

[Yury G. Kudryashov]

set_option autoImplicit true

[Jireh Loreaux]

The withType bit is about whether a proof term that appears in the infoview (as an _) displays with a type ascription or not. (i.e., _ vs. (_ : m = n), or whatever).

[Kyle Miller]

pp.proofs.withType is false by default now

[Kevin Buzzard]

I always turn on both autoImplicit and relaxedAutoImplicit. Can I get away with turning only one on?

[Kim Morrison]

#12689 remove the now redundany pp.proofs.withType setting in Mathlib's lakefile.

[Eric Wieser]

moreServerArgs is outdated now; https://github.com/ImperialCollegeLondon/FLT/pull/57 switches to the preferred leanOptions.

[Eric Wieser]

(and in fact, moreServerArgs does nothing if you don't use it in the lakefile!)

[Kevin Buzzard]

Oh that would explain why autoImplicits were on anyway! (and you can see from the resulting breakage why I need them off!)

[Eric Wieser]

Note that to see if my PR works, you have to click the "allow CI" button at the bottom of the page (or maybe "approve workflow")

[Shreyas Srinivas]

Without autoImplicits, you'll run into errors like the example below. The question is whether you consider this a reasonable trade off for your fellow contributors:

section experiment_1
set_option autoImplicit false
set_option relaxedAutoImplicit false

def compose (f : α → β) (g : β → γ) : α → γ := fun (x : α) => g (f x) -- errors on all \alpha, \beta, and \gamma
end experiment_1

def compose2 (f : α → β) (g : β → γ) : α → γ := fun (x : α) => g (f x) -- no errors