João Mendes (Apr 12 2022 at 20:08): João Mendes (Apr 12 2022 at 20:08):I am trying to install the version 6.2.3 of Coq so I can run this implementation, but it seems having camlp4 is necessary for it even though camlp4 is no longer actively maintained. Is there any way I can install this version of Coq without using camlp4?
It is also worth pointing that, despite the installation procedure file of coq 6.2.3 requires the OCaml compiler version 2.01, I am using OCaml current version, because when I run opam switch list-available 2.01 version is not listed
Karl Palmskog (Apr 12 2022 at 20:13):Coq version 6.X is over 20 years old. To my knowledge, even getting an OCaml environment that will support Coq < 8.X will require significant effort, and it's likely only the OCaml community that could help with that. Recent versions of OCaml will definitely not work.
Karl Palmskog (Apr 12 2022 at 20:19):see here for some surviving pieces of the universal algebra formalization that works on Coq 8.10: https://github.com/coq-contribs/prfx/blob/master/indices.v
João Mendes (Apr 12 2022 at 20:52):Fair enough :upside_down: . Many thanks for the help
Michael Soegtrop (Apr 13 2022 at 08:02):I also would think that most/all of the content of this package is available in modern Coq. @Enrico Tassi should have a good overview of what is available / missing.
Enrico Tassi (Apr 13 2022 at 08:05):In terms of features, I think everything is there. But porting the code is not easy since it is the pre 8.0 syntax...
IMO the best is to read the paper and re-do things. Looking at the website it does not seem a ton of code.
Enrico Tassi (Apr 13 2022 at 08:06):Given the topic, for sure @Cyril Cohen knows better what is available on the topic from other sources
Last updated: Oct 01 2023 at 19:01 UTC