Coqc 8.18 hangs when compiling "ott/coq/ott_list_flat_map.v"

[glynawe]

Coqc hangs when compiling "ott/coq/ott_list_flat_map.v". Vscoqtop does the same when editing it. Both end up using the entirety of one CPU and have to be killed.

I am using Ubuntu 22.04.4 LTS. I found this happens with Coq 8.18.0 and Coq 8.19.2.

With a bit of experimenting, I've found that it is the "autorewrite with lists" command that does it.

I don't know if this as fault in Ott's Coq library or Coq itself, sorry.

(Ott's Coq library is for an old version of Coq, I'm not sure which one. I've been trying to update it for myself. Successfully, until I reached ott_list_flat_map.v)

[palmskog]

@glynawe the only supported way of building the Coq library is by using Make and having coq_makefile installed (comes with Coq) and running make in the coq subdirectory of the Ott repository. This works fine for me with Coq 8.18, so your error very likely is due to Vscoq/vscoqtop. Ott is part of the Coq Platform, which is the recommended way of installing the Coq library for Ott.

There is an update in the works for 8.19, please see #105

[glynawe]

Thank you, I've switched to Coq Platform and aren't having trouble now. I was using Coq compiled with Ocaml 5.0.0 before, if that's significant. I have made a (maybe unnecessary) version of the Ott Coq library that has small changes to compile without warnings in 8.18 and work with vscoqtop, if you want it.

[palmskog]

Closing since we are unable to reproduce this and Ott is included in Platform using Coq 8.18.