Meven Lennon-Bertrand (Apr 08 2021 at 17:04): 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)?
Matthieu Sozeau (Apr 08 2021 at 17:19):You point to the right hoqidetop and you should be good to go
Théo Zimmermann (Apr 08 2021 at 17:19):Very soon you should be able to just use a _CoqProject file instead.
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?
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
Matthieu Sozeau (Apr 08 2021 at 17:21):Let me check what it installed :)
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.
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
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
Matthieu Sozeau (Apr 08 2021 at 17:25):In the meantime you just need to point to hoqidetop, certainly in your .opam/bin
Matthieu Sozeau (Apr 08 2021 at 17:25):In "settings/coqtop bin path"
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?
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: Jun 04 2023 at 23:30 UTC