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

leantar filename #5984

Closed
Eagle941 opened this issue Jul 18, 2023 · 0 comments
Closed

leantar filename #5984

Eagle941 opened this issue Jul 18, 2023 · 0 comments

Comments

@Eagle941
Copy link

Eagle941 commented Jul 18, 2023

Just created a new Lean project with the latest version of mathlib4 and typed lake exe cache get, I tried lake exe cache get!.

I got the error

leantar is too old; downloading more recent version
uncaught exception: no such file or directory (error code: 2)

The folder .cache contained leantar-0.1.3.exe.zip and leantar.exe.
Looking at the code, it seems like the expected filename shall contain the version (i.e. leantar-0.1.3.exe).

/-- leantar version at https://github.com/digama0/leangz -/
def LEANTARVERSION :=
  "0.1.3"

def LEANTARBIN :=
  -- change file name if we ever need a more recent version to trigger re-download
  IO.CACHEDIR / s!"leantar-{LEANTARVERSION}{if System.Platform.isWindows then ".exe" else ""}"

I manually renamed leantar.exe to leantar-0.1.3.exe and everything worked smoothly.

mathlib4 commit: ea67efc
lean4 toolchain: leanprover/lean4:nightly-2023-07-12

Can you replicate this issue?

@Eagle941 Eagle941 changed the title leantar leantar filename Jul 18, 2023
digama0 added a commit that referenced this issue Jul 18, 2023
@bors bors bot closed this as completed in 26d0eab Jul 19, 2023
semorrison pushed a commit that referenced this issue Aug 14, 2023
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

Successfully merging a pull request may close this issue.

1 participant