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
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.
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
Fair enough :upside_down: . Many thanks for the help
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.
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.
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