Stream: VsCoq devs & users

Topic: HoTT library


view this post on Zulip Meven Lennon-Bertrand (Apr 08 2021 at 17:04):

Hi! What is the current way to use VsCoq with the HoTT library (installed using opam)?

view this post on Zulip Matthieu Sozeau (Apr 08 2021 at 17:19):

You point to the right hoqidetop and you should be good to go

view this post on Zulip Théo Zimmermann (Apr 08 2021 at 17:19):

Very soon you should be able to just use a _CoqProject file instead.

view this post on Zulip Matthieu Sozeau (Apr 08 2021 at 17:20):

There has been recent work in the 8.13 branch where you just need to set the proper args, I'm not sure which version you installed ? 8.13.dev I suppose?

view this post on Zulip Meven Lennon-Bertrand (Apr 08 2021 at 17:20):

I’m trying to get a working install for the EPIT so very soon might not be soon enough ;) And yes I’m talking about 8.13.dev

view this post on Zulip Matthieu Sozeau (Apr 08 2021 at 17:21):

Let me check what it installed :)

view this post on Zulip Meven Lennon-Bertrand (Apr 08 2021 at 17:22):

To be more specific with the issue, I get a Cannot find a physical path bound to logical path matching suffix <> and prefix HoTT. error when using From HoTT Require Import HoTT.

view this post on Zulip Matthieu Sozeau (Apr 08 2021 at 17:23):

Ah, it checks out a tag " git+https://github.com/HoTT/HoTT.git#V8.13" which doesn't have the new stuff

view this post on Zulip Matthieu Sozeau (Apr 08 2021 at 17:24):

The new package is waiting for approval at https://github.com/coq/opam-coq-archive/pull/1671

view this post on Zulip Matthieu Sozeau (Apr 08 2021 at 17:25):

In the meantime you just need to point to hoqidetop, certainly in your .opam/bin

view this post on Zulip Matthieu Sozeau (Apr 08 2021 at 17:25):

In "settings/coqtop bin path"

view this post on Zulip Meven Lennon-Bertrand (Apr 08 2021 at 17:35):

It did something! But now I get an error on notation levels upon import Level 40 is already declared right associative while it is now expected to be left associative.… I guess this is not a VsCoq problem anymore?

view this post on Zulip Meven Lennon-Bertrand (Apr 08 2021 at 17:40):

Ah wait, I guess this is a conflict with the standard library? So I’m importing something behind the scene that I should not be importing.


Last updated: Jan 30 2023 at 18:04 UTC