Zulip Chat Archive
Stream: general
Topic: problem
夏目ヒカル (Jul 26 2022 at 12:02):
Snipaste_2022-07-26_19-58-31.jpg how to solve
Kevin Buzzard (Jul 26 2022 at 12:35):
Use leanproject for lean 3 repos
Eric Wieser (Jul 26 2022 at 12:39):
leanpkg should be working fine there
Eric Wieser (Jul 26 2022 at 12:40):
But it's impossible to help without knowing the layout of your files
夏目ヒカル (Jul 26 2022 at 12:52):
Kevin Buzzard said:
Use
leanprojectfor lean 3 repos
Snipaste_2022-07-26_20-51-38.jpg emm,now it like this
夏目ヒカル (Jul 26 2022 at 12:54):
Eric Wieser said:
But it's impossible to help without knowing the layout of your files
├─bin
├─tmp
├─toolchains
│ ├─leanprover-community--lean---3.45.0
│ │ ├─bin
│ │ ├─include
│ │ │ └─lean_ext
│ │ │ ├─checker
│ │ │ ├─frontends
│ │ │ │ └─lean
│ │ │ ├─init
│ │ │ ├─kernel
│ │ │ │ ├─inductive
│ │ │ │ └─quotient
│ │ │ ├─library
│ │ │ │ ├─compiler
│ │ │ │ ├─constructions
│ │ │ │ ├─equations_compiler
│ │ │ │ ├─inductive_compiler
│ │ │ │ ├─native_compiler
│ │ │ │ ├─predict
│ │ │ │ ├─tactic
│ │ │ │ │ ├─backward
│ │ │ │ │ └─smt
│ │ │ │ └─vm
│ │ │ ├─shell
│ │ │ └─util
│ │ │ ├─numerics
│ │ │ └─sexpr
│ │ └─lib
│ │ └─lean
│ │ ├─leanpkg
│ │ │ └─leanpkg
│ │ └─library
│ │ ├─data
│ │ │ └─buffer
│ │ ├─init
│ │ │ ├─algebra
│ │ │ ├─control
│ │ │ ├─data
│ │ │ │ ├─array
│ │ │ │ ├─bool
│ │ │ │ ├─char
│ │ │ │ ├─fin
│ │ │ │ ├─int
│ │ │ │ ├─list
│ │ │ │ ├─nat
│ │ │ │ ├─option
│ │ │ │ ├─ordering
│ │ │ │ ├─sigma
│ │ │ │ ├─string
│ │ │ │ ├─subtype
│ │ │ │ ├─sum
│ │ │ │ └─unsigned
│ │ │ └─meta
│ │ │ ├─converter
│ │ │ ├─lean
│ │ │ ├─smt
│ │ │ └─widget
│ │ ├─smt
│ │ ├─system
│ │ └─tools
│ │ └─debugger
│ └─stable
│ ├─bin
│ ├─include
│ │ └─lean_ext
│ │ ├─checker
│ │ ├─frontends
│ │ │ └─lean
│ │ ├─init
│ │ ├─kernel
│ │ │ ├─inductive
│ │ │ └─quotient
│ │ ├─library
│ │ │ ├─compiler
│ │ │ ├─constructions
│ │ │ ├─equations_compiler
│ │ │ ├─inductive_compiler
│ │ │ ├─native_compiler
│ │ │ ├─predict
│ │ │ ├─tactic
│ │ │ │ ├─backward
│ │ │ │ └─smt
│ │ │ └─vm
│ │ ├─shell
│ │ └─util
│ │ ├─numerics
│ │ └─sexpr
│ └─lib
│ └─lean
│ ├─leanpkg
│ │ └─leanpkg
│ └─library
│ ├─data
│ │ └─buffer
│ ├─init
│ │ ├─algebra
│ │ ├─control
│ │ ├─data
│ │ │ ├─array
│ │ │ ├─bool
│ │ │ ├─char
│ │ │ ├─fin
│ │ │ ├─int
│ │ │ ├─list
│ │ │ ├─nat
│ │ │ ├─option
│ │ │ ├─ordering
│ │ │ ├─sigma
│ │ │ ├─string
│ │ │ ├─subtype
│ │ │ ├─sum
│ │ │ └─unsigned
│ │ └─meta
│ │ ├─converter
│ │ ├─lean
│ │ ├─smt
│ │ └─widget
│ ├─smt
│ ├─system
│ └─tools
│ └─debugger
└─update-hashes
this?
Eric Wieser (Jul 26 2022 at 12:55):
Where is the tuto project? What's in your leanpkg.toml?
夏目ヒカル (Jul 26 2022 at 12:57):
Eric Wieser said:
Where is the tuto project? What's in your
leanpkg.toml?
in the root;
[package]
name = "leanpkg"
version = "0.1"
Eric Wieser (Jul 26 2022 at 14:16):
Not that one, the one that says name = "tuto"
Eric Wieser (Jul 26 2022 at 14:17):
夏目ヒカル said:
Eric Wieser said:
But it's impossible to help without knowing the layout of your files
this?
These are not your files, these are the ones that are installed by lean. I'm asking about the files that you are trying to build in this tuto project
Qihao Chen (Jul 26 2022 at 14:41):
Eric Wieser said:
夏目ヒカル said:
Eric Wieser said:
But it's impossible to help without knowing the layout of your files
this?
These are not your files, these are the ones that are installed by lean. I'm asking about the files that you are trying to build in this
tutoproject
I just installed lean.i did not bulid tuto https://leanprover-community.github.io/install/windows.html
Eric Wieser (Jul 26 2022 at 18:52):
Your original message says "configuring tuto 0.1"
Eric Wieser (Jul 26 2022 at 18:53):
"tuto" is not a lean thing, nor are any of our tutorials called "tuto"
Eric Wieser (Jul 26 2022 at 18:53):
So what is this "tuto" project?
Last updated: Dec 20 2023 at 11:08 UTC