Stream: SerAPI

Topic: ✔ type-in-type


view this post on Zulip Eben Rogers (Mar 14 2023 at 15:43):

Does unfortunately does not seem to work. I get the error as described in this issue: https://github.com/UniMath/UniMath/issues/648#issuecomment-285692878. So it seems that setting this flag does not work. This persists even if I unset the flag in the file PartA.v itself... :(

For anyone curious, this is the command I'm currently running alongside the modification to Init.v

view this post on Zulip Emilio Jesús Gallego Arias (Mar 14 2023 at 16:01):

What version are you using ? @Eben Rogers ?

view this post on Zulip Eben Rogers (Mar 14 2023 at 16:05):

Alectryon v1.4.0
The Coq Proof Assistant, version 8.16.1
sertop --version: 8.16.0+0.16.3

view this post on Zulip Emilio Jesús Gallego Arias (Mar 14 2023 at 16:17):

Easiest may be to add a --type-in-type option to SerAPI then

view this post on Zulip Eben Rogers (Mar 14 2023 at 17:11):

It seems I had to recompile the coq source code (which in hindsight seems obvious) in order to get alectryon and serapi to cooperate. So I (tentatively) think I've got it working. Thanks for all of the help!

view this post on Zulip Notification Bot (Mar 14 2023 at 17:11):

Eben Rogers has marked this topic as resolved.


Last updated: Apr 21 2024 at 01:02 UTC