Zulip Chat Archive

Stream: general

Topic: leanproject get-m --rev

Bolton Bailey (Feb 16 2022 at 19:09):

I was working with my mentee today and I was surprised to see that when I had him use leanproject get-m --rev origin/master, he got an error message, saying that this command had no --rev option. leanproject get-m -h confirmed this. He was using leanproject, version 1.1.0, whereas I use leanproject, version 1.0.0. DId something change between these versions to remove this option? How can I get this effect with this version of leanproject?

Eric Wieser (Feb 16 2022 at 19:16):

Use get-c not get-m

Eric Wieser (Feb 16 2022 at 19:18):

get-cache means "get the cache for the current lean project" (aka consult azure if the current project is mathlib, else look for a cache locally)

Eric Wieser (Feb 16 2022 at 19:19):

get-mathlib-cache means "get a fresh copy of mathlib in my _target directory of some non-mathlib project"

Last updated: Aug 03 2023 at 10:10 UTC