Zulip Chat Archive

Stream: general

Topic: lean hott


view this post on Zulip Johan Commelin (Mar 13 2020 at 13:31):

There is some form of HoTT for Lean 3. @Gabriel Ebner I think you know more about this.
With all our new cool tools, can I now easily work on this in one directory, and after that seamlessly switch VS code to a mathlib project?
Can leanproject support HoTT? Or does it already do it by chance?

view this post on Zulip Gabriel Ebner (Mar 13 2020 at 13:35):

The hott3 project doesn't require any modifications to Lean. There is a @[hott] attribute that forbids the use of eq.rec and heq.rec, and that's it.

view this post on Zulip Gabriel Ebner (Mar 13 2020 at 13:36):

However, as soon as you forbid eq.rec you can essentially say goodbye to the core library (or mathlib). You can use the same list, nat, prod, etc. But you can't reuse any theorems.

view this post on Zulip Gabriel Ebner (Mar 13 2020 at 13:37):

If you want to check it out, you can just leanproject get gebner/hott3.

view this post on Zulip Gabriel Ebner (Mar 13 2020 at 13:37):

I've just added a lean_version field so that elan should pick up the right lean version.

view this post on Zulip Gabriel Ebner (Mar 13 2020 at 13:40):

You also need to say goodbye to lots of built-in features such as cases or rw or the equation compiler (in general, it still works for lists and natural numbers and such). So we have eq_cases, hinduction, hsimp, hintro.

view this post on Zulip Johan Commelin (Mar 13 2020 at 13:51):

Cloning from https://github.com/gebner/hott3.git
error: override toolchain 'leanprover-community/lean:3.7.0' is not installed
info: caused by: the toolchain file at '/home/jmc/data/math/hott3/leanpkg.toml' specifies an uninstalled toolchain

Should leanproject install this for me automatically?

view this post on Zulip Johan Commelin (Mar 13 2020 at 13:51):

Or do we want users to ask elan to do this

view this post on Zulip Gabriel Ebner (Mar 13 2020 at 13:53):

Are you by any chance on windows? The 3.7.0 builds will probably take another hour or so.

view this post on Zulip Johan Commelin (Mar 13 2020 at 13:54):

Nope... linux :penguin:

view this post on Zulip Gabriel Ebner (Mar 13 2020 at 13:55):

Mmmh, then it should work out of the box. And if doesn't, then mathlib will break for you as well soon.

view this post on Zulip Gabriel Ebner (Mar 13 2020 at 13:56):

Did you need to do anything for the mathlib upgrade to 3.6.0?

view this post on Zulip Johan Commelin (Mar 13 2020 at 13:56):

I haven't done that yet on this box. Let me try.

view this post on Zulip Johan Commelin (Mar 13 2020 at 13:59):

@Gabriel Ebner

(error: override toolchain 'leanprover-community/lean:3.6.1' is not installed, the toolchain file at '/home/jmc/data/math/mathlib/leanpkg.toml' specifies an uninstalled toolchain)

view this post on Zulip Johan Commelin (Mar 13 2020 at 13:59):

Maybe my elan is really old...

view this post on Zulip Gabriel Ebner (Mar 13 2020 at 13:59):

I think elan can update itself.

view this post on Zulip Gabriel Ebner (Mar 13 2020 at 13:59):

elan self update

view this post on Zulip Gabriel Ebner (Mar 13 2020 at 13:59):

Does this work for you?

view this post on Zulip Johan Commelin (Mar 13 2020 at 13:59):

$ elan self update
info: checking for self-updates
info: downloading self-update
Error(Download(HttpStatus(404)), State { next_error: None, backtrace: None })
error: could not download file from 'https://github.com/Kha/elan/releases/download/v0.8.0","user_id":null%7D%7D/elan-x86_64-unknown-linux-gnu.tar.gz' to '/tmp/elan-update.xzw5tBCb62Kj/elan-x86_64-unknown-linux-gnu.tar.gz'
info: caused by: http request returned an unsuccessful status code: 404

view this post on Zulip Gabriel Ebner (Mar 13 2020 at 14:00):

@Sebastian Ullrich This looks like an elan bug ^^

view this post on Zulip Gabriel Ebner (Mar 13 2020 at 14:00):

I guess you need to reinstall elan.

view this post on Zulip Koundinya Vajjha (Mar 13 2020 at 14:00):

FWIW, I get the same error too.

view this post on Zulip Sebastian Ullrich (Mar 13 2020 at 14:01):

Huh, I guess HTML parsing isn't very stable after all

view this post on Zulip Marc Huisinga (Mar 13 2020 at 14:04):

Sebastian Ullrich said:

I parse HTML using regexes, of course

view this post on Zulip Johan Commelin (Mar 13 2020 at 14:05):

he comes he comes do not fi​ght he com̡e̶s, ̕h̵i​s un̨ho͞ly radiańcé destro҉ying all enli̍̈́̂̈́ghtenment, HTML tags lea͠ki̧n͘g fr̶ǫm ̡yo​͟ur eye͢s̸ ̛l̕ik͏e liq​uid pain, the song of re̸gular exp​ression parsing will exti​nguish the voices of mor​tal man from the sp​here I can see it can you see ̲͚̖͔̙î̩́t̲͎̩̱͔́̋̀ it is beautiful t​he final snuffing of the lie​s of Man ALL IS LOŚ͖̩͇̗̪̏̈́T ALL I​S LOST the pon̷y he comes he c̶̮omes he comes the ich​or permeates all MY FACE MY FACE

view this post on Zulip Marc Huisinga (Mar 13 2020 at 14:11):

even joking about it will attract h̵i​s wrath

view this post on Zulip Johan Commelin (Mar 13 2020 at 14:18):

@Gabriel Ebner Reinstalling elan helped

view this post on Zulip Sebastian Ullrich (Mar 13 2020 at 14:30):

@Johan Commelin Does the error persist after the manual update?

view this post on Zulip Johan Commelin (Mar 13 2020 at 14:31):

No, it seems to be gone.

view this post on Zulip Johan Commelin (Mar 13 2020 at 14:31):

My CPU's are currently maxing out while checking cubical/*.lean

view this post on Zulip Sebastian Ullrich (Mar 13 2020 at 14:32):

Great, then the bug has been long fixed

view this post on Zulip Johan Commelin (Mar 13 2020 at 14:40):

@Gabriel Ebner Currently master contains sorry. Do you have any idea how hard it would be to make it sorry-free?

view this post on Zulip Gabriel Ebner (Mar 13 2020 at 14:44):

hott3 is pretty much unmaintained. @Floris van Doorn has been merging a lot of PRs, but I don't think anybody actually has a use for it.

view this post on Zulip Gabriel Ebner (Mar 13 2020 at 14:45):

Also hott3 is far from "finished". Most of the files are a direct port of the Lean 2 HoTT library. But only like 5% is ported. The sorry should be the least of your worries.

view this post on Zulip Johan Commelin (Mar 13 2020 at 15:06):

Is it at all reasonable to think that we can try to prove quadratic reciprocity in HoTT3?

view this post on Zulip Johan Commelin (Mar 13 2020 at 15:06):

Or should we switch to cubical agda, or something similar, if we want to do such an experiment?

view this post on Zulip Gabriel Ebner (Mar 13 2020 at 15:21):

Other people are probably more qualified than me to answer this question. hott3 is at a point where I think you could try this experiment (if you have way too much free time). On the plus side, there is a simplifier and you already know the syntax. If I wanted to it, I would probably also look at other HoTT systems with mathematical libraries first, such as the HoTT library in Coq. I wouldn't do it in cubical Agda, because AFAICT there are no tactics and I wouldn't want to work without rw or simp.


Last updated: May 14 2021 at 07:19 UTC