Stream: VsCoq devs & users

Topic: HoTT


view this post on Zulip Ramkumar Ramachandra (May 28 2020 at 14:21):

#97 doesn't work for me anymore, due to an opam upgrade this morning. I don't know which version of coq and coq-hott it's supposed to work with. I currently have coq.8.11.1 and coq-hott.8.11 installed.

view this post on Zulip Ramkumar Ramachandra (May 28 2020 at 14:27):

"Interpret to point failed: Error: Request coqtop/interpretToPoint failed unexpectedly without providing any details."

view this post on Zulip Ramkumar Ramachandra (May 28 2020 at 14:32):

Sorry, the diagnosis was incorrect: I'd also pulled HoTT, which needed a rebuild.

view this post on Zulip vlj (Jun 04 2020 at 19:32):

It's possible to use vscoq with hoqtop ?

view this post on Zulip Ramkumar Ramachandra (Jun 05 2020 at 06:10):

Yes, I'm using it successfully with #97.

view this post on Zulip Ramkumar Ramachandra (Jun 05 2020 at 06:13):

I've been trying to get @Maxime Dénès to merge it into vscoq.


Last updated: Jan 30 2023 at 18:04 UTC