ZFSet typing problem

Stream: new members

[Bbbbbbbbba]

On the web playground this seems to work fine:

import Mathlib

def is_omega (x : ZFSet) : Prop := x = {{}} ∪ { insert y y | y ∈ x }

However, on my local installation of lean, I get an error:

type mismatch
  {∅} ∪ {x_1 | ∃ y ∈ x, insert y y = x_1}
has type
  Set ZFSet : Type (?u.2 + 1)
but is expected to have type
  ZFSet : Type (?u.2 + 1)

Is this because my local versions are old? How should I update?

[Miyahara Kō]

To update your Mathlib, prease refer to this page.

[Bbbbbbbbba]

Miyahara Kō said:

To update your Mathlib, prease refer to this page.

I am trying to update, but lake update seems to be stuck for a few minutes without any terminal output...

[Bbbbbbbbba]

I finally got an error :sad: error: external command 'git' exited with code 128

[Miyahara Kō]

Git error? It may be caused by bad internet connection.

[Bbbbbbbbba]

Yeah my connection to github is really bad. Is there a "manual" method?

[Miyahara Kō]

I think there is no easy manual method, because lake update process is made up of two process: downloading new dependent repositories, and downloading their caches.
Downloading repositories may be easy, but downloading chaches is fairly complicated process.

[Bbbbbbbbba]

Also after updating the lean-toolchain everything is broken. Is this normal? Is lake update supposed to fix this?

`/Users/bbbbbbbbba/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/bin/lake setup-file /Users/bbbbbbbbba/lean/playground/Playground/Temp copy.lean - --no-build --no-cache` failed:

stderr:
error: /Users/bbbbbbbbba/lean/playground/.lake/packages/proofwidgets/lakefile.lean:22:20: Type mismatch
  inputFile (widgetDir / { toString := "package.json" })
has type
  Bool → SpawnM (Job FilePath)
but is expected to have type
  FetchM ?m.14
warning: /Users/bbbbbbbbba/lean/playground/.lake/packages/proofwidgets/lakefile.lean:33:36: `_package.name` has been deprecated: Use `__name__` instead.
error: /Users/bbbbbbbbba/lean/playground/.lake/packages/proofwidgets/lakefile.lean:33:71: Unknown constant `IO.Mutex`
error: /Users/bbbbbbbbba/lean/playground/.lake/packages/proofwidgets/lakefile.lean:34:38: Function expected at
  BuildJob
but this term has type
  ?m.1

Note: Expected a function because this term is being applied to the argument
  FilePath

Hint: The identifier `BuildJob` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be a function, and a function is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement.
error: /Users/bbbbbbbbba/lean/playground/.lake/packages/proofwidgets/lakefile.lean:35:12: Function expected at
  BuildJob
but this term has type
  ?m.1

Note: Expected a function because this term is being applied to the argument
  FilePath

Hint: The identifier `BuildJob` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be a function, and a function is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement.
error: /Users/bbbbbbbbba/lean/playground/.lake/packages/proofwidgets/lakefile.lean:37:2: Unknown identifier `buildFileAfterDepArray`
warning: /Users/bbbbbbbbba/lean/playground/.lake/packages/proofwidgets/lakefile.lean:69:38: `_package.name` has been deprecated: Use `__name__` instead.
error: /Users/bbbbbbbbba/lean/playground/.lake/packages/proofwidgets/lakefile.lean:70:12: Function expected at
  BuildJob
but this term has type
  ?m.1

Note: Expected a function because this term is being applied to the argument
  (Array FilePath)

Hint: The identifier `BuildJob` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be a function, and a function is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement.
error: /Users/bbbbbbbbba/lean/playground/.lake/packages/proofwidgets/lakefile.lean:78:25: Unknown constant `IO.Mutex.new`
error: /Users/bbbbbbbbba/lean/playground/.lake/packages/proofwidgets/lakefile.lean:80:2: Invalid field notation: Field projection operates on types of the form `C ...` where C is a constant. The expression
  BuildJob
has type `x✝` which does not have the necessary form.
error: /Users/bbbbbbbbba/lean/playground/.lake/packages/proofwidgets/lakefile.lean:76:36: Application type mismatch: The argument
  inputFile
has type
  FilePath → Bool → SpawnM (Job FilePath)
but is expected to have type
  FilePath → ?m.148 fs (Job (CustomOut (widgetPackageLock.pkg, widgetPackageLock.name)))
in the application
  Array.mapM inputFile
warning: /Users/bbbbbbbbba/lean/playground/.lake/packages/proofwidgets/lakefile.lean:82:7: declaration uses 'sorry'
warning: /Users/bbbbbbbbba/lean/playground/.lake/packages/proofwidgets/lakefile.lean:85:7: declaration uses 'sorry'
error: /Users/bbbbbbbbba/lean/playground/.lake/packages/proofwidgets/lakefile.lean: package configuration has errors
Failed to configure the Lake workspace. Please restart the server after fixing the error above.

[Miyahara Kō]

This is probably normal. When you update lean-toolchain, you have to update dependencies in lake-manifest.json. This update is done by lake update.

[Notification Bot]

10 messages were moved here from #new members > Just saying hi by Matt Diamond.