I tried using this library with the following code in my lakefile.toml:
[[require]]
name = "lean4-assert-command"
scope = "pnwamk"
As I understand it, this is how you usually download packages.
After lake update lean4-assert-command I got the error:
error: 'lean4-assert-command' was downloaded incorrectly; you will need to manually delete '.\.\.lake\packages\lean4-assert-command': permission denied (error code: 13)
file: .\.\.lake\packages\lean4-assert-command\.git\objects\pack\pack-e8d491957b1e75ee8ff653eacbc99400741c1385.idx
error: interpreter: package 'assertCmd' was required as 'lean4-assert-command'
I tried changing the lakefile to
[[require]]
name = "assertCmd"
scope = "pnwamk"
but I got package not found on Reservoir.
At the end I managed to use it with
name = "assertCmd"
scope = "pnwamk"
git = "https://github.com/pnwamk/lean4-assert-command"
but this is not ideal as I would rather use the reservoir.
If you know how, could you please let me know how to [[require]] your package? Thank you
I tried using this library with the following code in my
lakefile.toml:As I understand it, this is how you usually download packages.
After
lake update lean4-assert-commandI got the error:I tried changing the lakefile to
but I got
package not found on Reservoir.At the end I managed to use it with
but this is not ideal as I would rather use the reservoir.
If you know how, could you please let me know how to [[require]] your package? Thank you