Hi! What is the current way to use VsCoq with the HoTT library (installed using opam)?
You point to the right hoqidetop and you should be good to go
Very soon you should be able to just use a
_CoqProject file instead.
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?
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
Let me check what it installed :)
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.
Ah, it checks out a tag " git+https://github.com/HoTT/HoTT.git#V8.13" which doesn't have the new stuff
The new package is waiting for approval at https://github.com/coq/opam-coq-archive/pull/1671
In the meantime you just need to point to
hoqidetop, certainly in your
In "settings/coqtop bin path"
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?
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