Zulip Chat Archive

Stream: new members

Topic: tutorials

Pedro Castilho (Nov 09 2020 at 19:02):

hi, i imported tutorials from leans GitHub repository but the flies don't work right away, it can't import tactic.suggest for exemple. Is there a way to solve this without needing to use leanproject new every time?

Shing Tak Lam (Nov 09 2020 at 19:04):

Hello, how did you download the tutorials from GitHub, did you use leanproject get or git?

Pedro Castilho (Nov 09 2020 at 19:11):

I used git

Johan Commelin (Nov 09 2020 at 19:13):

  1. @Pedro Castilho Do you have elan installed? (What does which elan say?)
  2. Once you are in the git repo, if you call leanproject get-mathlib-cache you should get precompiled binaries. This may help.
  3. What error do you get? What do you mean with "it can't import tactic.suggest"?
  4. leanproject get tutorials should make all of this a 1-liner, without needing to use leanproject new.

Pedro Castilho (Nov 09 2020 at 19:15):

yes I have it says /Users/pedro/.elan/bin/elan

Pedro Castilho (Nov 09 2020 at 19:16):

I get the following:

could not resolve import: tactic.suggest```

Johan Commelin (Nov 09 2020 at 19:18):

Did you open the folder in VScode? Or did you open a single file?

Pedro Castilho (Nov 09 2020 at 19:18):

only the file, is that it?

Ruben Van de Velde (Nov 09 2020 at 19:19):

Probably, yes

Johan Commelin (Nov 09 2020 at 19:19):

That might be the problem

Pedro Castilho (Nov 09 2020 at 19:19):

am going to try that

Johan Commelin (Nov 09 2020 at 19:19):

You can run code . inside the project directory, or choose File > Open Folder from the menu

Pedro Castilho (Nov 09 2020 at 19:20):

hahaha, thanks guys

Pedro Castilho (Nov 09 2020 at 19:20):

it worked

Last updated: Dec 20 2023 at 11:08 UTC