use hott3 library on windows

Stream: general

[Thomas Eckl]

I tried to use the hott3 library of Gabriel Ebner and Floris van Doorn for a project of my own. So I cloned the library, executed leanpkg build, created my own project with leanpkg, added the path to the hott3 library to leanpkg.path

[Thomas Eckl]

builtin_path
path ./src
path ../../hott3/src

and as a local dependency to leanpkg.toml

[package]
name = "HoTT-Case-Study"
version = "0.1"
path = "src"
lean_version = "leanprover-community/lean:3.7.0"

[dependencies]
# local dependency
hott3 = { path = "../../hott3" }

Still I can't import any files from the hott3 library: import hott.init just triggers file 'hott\init' not found in the search path . However the path is present when executing lean --path.

What am I doing wrong?

[Patrick Massot]

Do you really insist on doing this by hand?

[Patrick Massot]

Do you intend to modify the hott lib along the way?

[Patrick Massot]

You answered in the wrong thread.

[Patrick Massot]

Anyway, even if you want to do a lot by hand, modifying both those files is meaningless.

[Patrick Massot]

The toml file is meant to write the path file for you.

[Thomas Eckl]

Sorry. Well, the manual only tells me how to produce a leanpkg using mathlib - I don't want to do that. It might be that I have to extend the hott library; I want to port some Lean2 hott files and don't know yet what I need on the way.

[Reid Barton]

You shouldn't ever need to edit leanpkg.path: that's between leanpkg and lean.

[Thomas Eckl]

And how do you bring the toml file to include the path to the hott3 library?

[Reid Barton]

I would just use a git dependency probably.

[Patrick Massot]

Your toml looks fine

[Patrick Massot]

just use leanpkg configure after writing this toml

[Thomas Eckl]

Did it, no extra path included in leanpkg.path.

[Patrick Massot]

No, you didn't.

[Reid Barton]

what do you mean "extra"?

[Patrick Massot]

I'll list steps for you, hold on

[Patrick Massot]

• cd /tmp
• git clone git@github.com:gebner/hott3.git
• mkdir my_proj
• Inside my_proj/leanpkg.toml, write

[package]
name = "eckl"
version = "0.1"
lean_version = "leanprover-community/lean:3.7.0"
path = "src"

[dependencies]

hott3 = { path = "../hott3" }

• cd my_proj
• leanpkg configure
• mkdir src

[Patrick Massot]

• enjoy your leanpkg.path

[Reid Barton]

Just to check, you did open the project/folder/whatever it's called in VSCode, right?

[Thomas Eckl]

Worked! Thanks a lot! Now I am wondering: There are no .olean files in the hott3 folders. Do I need to leanpkg build them?

[Patrick Massot]

Yes, I don't think the hott3 team provides precompiled oleans.

[Patrick Massot]

I'm curious: where did you get the idea to edit leanpkg.path by hand?

[Patrick Massot]

I'm asking because we are always hunting down ancient obsolete instructions.

[Thomas Eckl]

Don't worry about ancient instructions: Because I didn't find any instructions at all for packages not depending on mathlib, I just thought that this might work.

[Thomas Eckl]

Should have read more about the workings of leanpkg I guess.

[Patrick Massot]

TBH, I don't think we have much doc about such an unusual situation.

[Patrick Massot]

99.99% of Lean project are either mathlib or depend on mathlib and nothing else.

[Thomas Eckl]

Zulip seems to be a good replacement for documentation :grinning:

[Patrick Massot]

I don't even remember whether I created a leanproject command to add a dependency which is not mathlib.

[Patrick Massot]

I think no.

[Patrick Massot]

Feel free to open a doc PR (or even a leanproject PR).

[Thomas Eckl]

I completely understand that the focus is on mathlib(-dependent projects). But I want to find out whether the nice ecosystem of Lean 3 makes experimenting with HoTT easier. Let's see ...

[Reid Barton]

leanpkg already has an option to do this. The instructions after git clone can be equivalently leanpkg new my_proj; cd my_proj; leanpkg install ../hott3; leanpkg configure (untested).

[Reid Barton]

It's documented insofar as leanpkg --help exists.

[Thomas Eckl]

Since I don't know what a doc PR is, Reid's remark seems a good final point. If my project runs to some fat I might get back to a leanproject PR.