Zulip Chat Archive

Stream: general

Topic: lean hott

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?

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.

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.

Gabriel Ebner (Mar 13 2020 at 13:37):

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

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.

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.

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?

Johan Commelin (Mar 13 2020 at 13:51):

Or do we want users to ask elan to do this

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.

Johan Commelin (Mar 13 2020 at 13:54):

Nope... linux :penguin:

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.

Gabriel Ebner (Mar 13 2020 at 13:56):

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

Johan Commelin (Mar 13 2020 at 13:56):

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

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)

Johan Commelin (Mar 13 2020 at 13:59):

Maybe my elan is really old...

Gabriel Ebner (Mar 13 2020 at 13:59):

I think elan can update itself.

Gabriel Ebner (Mar 13 2020 at 13:59):

elan self update

Gabriel Ebner (Mar 13 2020 at 13:59):

Does this work for you?

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

Gabriel Ebner (Mar 13 2020 at 14:00):

@Sebastian Ullrich This looks like an elan bug ^^

Gabriel Ebner (Mar 13 2020 at 14:00):

I guess you need to reinstall elan.

Koundinya Vajjha (Mar 13 2020 at 14:00):

FWIW, I get the same error too.

Sebastian Ullrich (Mar 13 2020 at 14:01):

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

Marc Huisinga (Mar 13 2020 at 14:04):

Sebastian Ullrich said:

I parse HTML using regexes, of course

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

Marc Huisinga (Mar 13 2020 at 14:11):

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

Johan Commelin (Mar 13 2020 at 14:18):

@Gabriel Ebner Reinstalling elan helped

Sebastian Ullrich (Mar 13 2020 at 14:30):

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

Johan Commelin (Mar 13 2020 at 14:31):

No, it seems to be gone.

Johan Commelin (Mar 13 2020 at 14:31):

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

Sebastian Ullrich (Mar 13 2020 at 14:32):

Great, then the bug has been long fixed

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?

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.

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.

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?

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?

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: Dec 20 2023 at 11:08 UTC