Zulip Chat Archive

Stream: lean4

Topic: 10-20 update

Mario Carneiro (Oct 20 2022 at 10:34):

Attn lean 4 package maintainers: @Xubai Wang , @Marc Huisinga , @Henrik Böving , @Mac , @Gabriel Ebner : The 10-20 nightly broke every lake package (mainly because the @[defaultTarget] attribute used in every lakefile is now spelled @[default_target], mea culpa), so I'm working on getting the updates deployed as quickly as possible to minimize disruption. I sent PRs to all the dependencies of mathlib, although doc-gen4 and LeanInk repos seem to have a more complicated setup and I may not have sent the PR to the right branch.

Sebastian Ullrich (Oct 20 2022 at 10:35):

TPiL4 broke as well https://github.com/leanprover/theorem_proving_in_lean4/actions/runs/3288702869

Jannis Limperg (Oct 20 2022 at 11:57):

Some more subtle breakage: any uses of isAuxDecl likely have to be replaced with isImplementationDetail. (Don't know how recent this change is.)

François G. Dorais (Oct 20 2022 at 12:02):

Why this change?

Mario Carneiro (Oct 20 2022 at 12:16):

It's not just a name change, auxDecl was a binder info and isImplementationDetail is a function on Name

Arthur Paulino (Oct 20 2022 at 12:45):

CC @Daniel Rogozin @Ilona Prikule @cognivore @Matej Penciak for when we're bumping toolchains

Jannis Limperg (Oct 20 2022 at 13:22):

Mario Carneiro said:

It's not just a name change, auxDecl was a binder info and isImplementationDetail is a function on Name

More specifically:

  • auxDecl is not a BinderInfo any more.
  • LocalDecl has a new field LocalDeclKind, which can be one of default, implDetail and auxDecl.
  • Hypotheses of auxDecl or implDetail kind are supposed to be ignored by tactics which iterate over the local context. So a typical for loop which filters hypotheses via isAuxDecl is now broken and needs to filter via isImplementationDetail instead (where isImplementationDetail is true for both auxDecl and implDetail hyps).

Gabriel Ebner (Oct 20 2022 at 16:05):

What Jannis said. Also, Name.isImplementationDetail is only used by elaborators to decide whether variables should be marked as LocalDeclKind.implDetail. Tactics should not use Name.isImplementationDetail.

Henrik Böving (Oct 20 2022 at 16:29):

I'll looking into fixing doc-gen again for today's mathlib version then yes?

Henrik Böving (Oct 20 2022 at 17:47):

What happened to Name.components'?

Mario Carneiro (Oct 20 2022 at 17:48):

it's componentsRev now

Mario Carneiro (Oct 20 2022 at 17:49):

you got my PR leanprover/doc-gen4#86, right?

Mario Carneiro (Oct 20 2022 at 17:49):

I think I fixed all those issues in it

Henrik Böving (Oct 20 2022 at 17:51):

Oh I was going through the changes myself as you sent this it seems haha. I already updated all the dependencies as well so this should hopefully work...

Henrik Böving (Oct 20 2022 at 17:52):

Yup, it compiles :thumbs_up:

Tomas Skrivan (Oct 21 2022 at 10:34):

I didn't update my manifest.json or lean-toolchain and yet I'm getting error

./lean_packages/std/lakefile.lean:9:2: error: unknown attribute [default_target]

How come std got upgraded?

Last updated: Dec 20 2023 at 11:08 UTC