Eben Rogers (Mar 14 2023 at 14:50): Eben Rogers (Mar 14 2023 at 14:50):Hi, I'm currently trying to compile the UniMath library using Alectryon (which uses SerAPI behind the scenes) to create more readable documentation. Alectryon allows passing flags to to sertop using --sertop-arg. But I am unable to figure out what flag to pass on to sertop to allow it to compile coq using the -type-in-type flag. Is there some way to do this that I have missed so far? WIthout this flag, UniMath throws up errors when compiling.
Gaëtan Gilbert (Mar 14 2023 at 14:58):I don't know about serapi but you should be able to work around it by putting Global Unset Universe Checking. at the beginning of the first file (https://github.com/UniMath/UniMath/blob/master/UniMath/Foundations/Init.v AFAICT)
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
Emilio Jesús Gallego Arias (Mar 14 2023 at 16:01):What version are you using ? @Eben Rogers ?
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
Emilio Jesús Gallego Arias (Mar 14 2023 at 16:17):Easiest may be to add a --type-in-type option to SerAPI then
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!
Notification Bot (Mar 14 2023 at 17:11):Eben Rogers has marked this topic as resolved.
Last updated: Jun 11 2023 at 00:30 UTC