Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Documentation for Lean Version Upgrade #280

Open
agureev opened this issue Oct 18, 2023 · 0 comments
Open

Documentation for Lean Version Upgrade #280

agureev opened this issue Oct 18, 2023 · 0 comments

Comments

@agureev
Copy link

agureev commented Oct 18, 2023

Since Yatima is not currently in active development, it would be great to have documentation on how to upgrade the Lean version of the current project so that user may be able to still use compiler as the lake upgrade command suggested after lake run setup does not seem to bump everything properly.

Currently after pulling main and running lake run setup produces

warning: improperly formatted manifest: incompatible manifest version `4`
error: dependency 'LSpec' of 'Yatima' not in manifest, use `lake update` to update

while running lake update produces

warning: improperly formatted manifest: incompatible manifest version `4`
error: ./lake-packages/YatimaStdLib/lakefile.lean:14:15: error: invalid field 'oleanDir', the environment does not contain 'Lake.Package.oleanDir'
  pkg
has type
  Package
error: ./lake-packages/YatimaStdLib/lakefile.lean:23:33: error: unknown identifier 'defaultLibDir'
error: ./lake-packages/YatimaStdLib/lakefile.lean:23:57: error: application type mismatch
  List.cons job
argument
  job
has type
  CustomData (Package.name pkg, `importTarget) : Type
but is expected to have type
  BuildJob FilePath : Type
error: ./lake-packages/YatimaStdLib/lakefile.lean: package configuration has errors

Might be an issue with Lean4 Arch (AUR) package, however.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant