UnicodeBasic error when upgrading to 4.8.0rc2

Stream: lean4

[Ralf Stephan]

In my project directory, after changing in lean-toolchain from rc1 to leanprover/lean4:v4.8.0-rc2:

$ lake exe cache get
error: ././.lake/packages/UnicodeBasic/lakefile.lean:24:12: error: invalid field notation, function 'Lake.LogIO.captureLog' does not have argument with type (Lake.LogIO ...) that can be used, it must be explicit or implicit with a unique name
error: ././.lake/packages/UnicodeBasic/lakefile.lean: package configuration has errors

I remove the package directory .lake/packages/UnicodeBasic/ and try again,

info: UnicodeBasic: cloning https://github.com/fgdorais/lean4-unicode-basic to '././.lake/packages/UnicodeBasic'

and the same error comes up. How to fix?

[Kevin Buzzard]

I don't know anything about this stuff but my instinct is that you should post your lakefile.lean in full so people understand better what's happening in your situation.

[Ralf Stephan]

However, the lean version seems successfuly changed. Still...

[Ralf Stephan]

import Lake
open Lake DSL

package «infinite-primes-via-log» where
  -- Settings applied to both builds and interactive editing
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b`
  ]
  -- add any additional package configuration options here

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

@[default_target]
lean_lib «InfinitePrimesViaLog» where
  -- add any library configuration options here

require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git"

meta if get_config? env = some "dev" then
require «doc-gen4» from git
  "https://github.com/leanprover/doc-gen4" @ "main"

[Ralf Stephan]

This error prevents any file from compiling using rc2 here, so it is a problem.

[Ralf Stephan]

Maybe you meant I should post the UnicodeBasic/lakefile.lean?

/-
Copyright © 2023 François G. Dorais. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
-/

import Lake
open Lake DSL

package UnicodeBasic

@[default_target]
lean_lib UnicodeBasic {
  precompileModules := true
}

lean_exe UnicodeTool

/-- Update data files from the Unicode Character Database (UCD) -/
script UpdateUCD := do
  let dataDir : FilePath := "./data"
  for file in ["UnicodeData.txt", "PropList.txt"] do
    let url := "https://www.unicode.org/Public/UCD/latest/ucd/" ++ file
    IO.println s!"Downloading UCD/{file}"
    let _ ← download url (dataDir/file) |>.captureLog    -- <==== this
  return 0

[Richard Copley]

Commit your changes and/or make a backup (to make sure you can go back and try something else if necessary), then try lake update in the top-level project directory.

[Kevin Buzzard]

Just to be clear: I don't know what I mean, I just felt like more data might be helpful.

[Ralf Stephan]

Okay, after lake update several repos were updated, among them:

info: UnicodeBasic: updating repository '././.lake/packages/UnicodeBasic' to revision 'effd8b8771cfd7ece69db99448168078e113c61f'

Now files compile without error, thanks. I shall submit a PR adding something about updating in general to the community page install/project.html.

[Kevin Buzzard]

lake update is not a good solution for everyone: if people depend on mathlib and another repo which mathlib also relies on then lake update wil update everything and give possibly incompatible versions of dependencies. It's a very delicate issue and is constantly causing problems.

[Ralf Stephan]

Is there a page / thread where people can be pointed to for updating a project?

[Ruben Van de Velde]

I think there's a link from the main mathlib4 README about "depending on mathlib"

[Ralf Stephan]

https://github.com/leanprover-community/leanprover-community.github.io/pull/478

Please add/change if inaccurate.

[Yaël Dillies]

Kevin Buzzard said:

lake update is not a good solution for everyone: if people depend on mathlib and another repo which mathlib also relies on then lake update wil update everything and give possibly incompatible versions of dependencies. It's a very delicate issue and is constantly causing problems.

I don't think that's true anymore? Certainly lake update on PFR (which depends on APAP which depends on mathlib) works fine

[Kevin Buzzard]

Oh that's good to know! I'll try it on FLT next time and see what happens :-)

[Utensil Song]

Yaël Dillies said:

Kevin Buzzard said:

lake update is not a good solution for everyone: if people depend on mathlib and another repo which mathlib also relies on then lake update wil update everything and give possibly incompatible versions of dependencies. It's a very delicate issue and is constantly causing problems.

I don't think that's true anymore? Certainly lake update on PFR (which depends on APAP which depends on mathlib) works fine

You mean

curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake -R -Kenv=dev update

works fine, right? A raw lake update still bites.

[Utensil Song]

Your script dodges 3 delicate issues.

[Yaël Dillies]

Ah well maybe we should make my script the default :sweat_smile:

[Eric Wieser]

Kevin Buzzard said:

if people depend on mathlib and another repo which mathlib also relies on then lake update wil update everything and give possibly incompatible versions of dependencies.

This is still true, but also you shouldn't ever "depend on mathlib and another repo which mathlib also relies on" unless this incompatibility is actually what you want. If you have Mathlib in your lakefile, then you should not have Aesop or batteries or quote4 or ...

[Ruben Van de Velde]

I think the main situation that might be problematic is one where your have multiple independent direct dependencies that both depend on the same third package

[Eric Wieser]

Yes, but in that case any update at all is probably problematic, manual or otherwise

[François G. Dorais]

Quick update from the UnicodeBasic maintainer. It seems that the issue has been resolved but here are some details.

Updates to UnicodeBasic happen within a day of every lean core update, to the extent possible.

The underlying issue is due to lake's monad refactoring. This was patched in UnicodeBasic revision 2a272ebb3af6ce1bcd6c997a5675d674a839716e on May 21.

The UnicodeBasic requirement is from doc-gen4 which currently uses UnicodeBasic revision effd8b8771cfd7ece69db99448168078e113c61f, which includes the patch mentioned above.

Please let me know of any other issues with UnicodeBasic, or submit an issue at https://github.com/fgdorais/lean4-unicode-basic