search

damien-pous / coinduction

coinduction library for Coq
GNU Lesser General Public License v3.0
13 stars 4 forks source link

Support for 8.15 #6

Closed YaZko closed 2 years ago

YaZko commented 2 years ago

Hello,

Sorry to ask for more, but would it be possible to support 8.15? The coq part of the development works, but there seems to have been some change in the OCaml API (?), the reification is failing. But I've never build a plugin, there must be basic things I don't understand, as I'm not sure why it fails differently with make and building through opam. With make it straight up seems to not be called with the right arguments anymore and fails as:

File "reification_i.ml", line 2, characters 8-30:
2 | let _ = Mltop.add_known_module __coq_plugin_name
            ^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound module Mltop

While with opam it's a type errror:

# File "reification_i.mlg", line 25, characters 64-82:
# Error: This expression has type Names.GlobRef.t
#        but an expression was expected of type Environ.env

Best, Yannick

damien-pous commented 2 years ago

Hi @YaZko,

Added support for v8.15... in the new v8.15 branch (incompatible change in the API). Be careful to [make cleanall] before recompiling : the first error you mention seems to arise when there are old compiled files around, preventing their recompilation.

Now I have to understand how to opam the two versions... (possibly I'll do one as is for 8.14, then a new one for 8.15, and I'll continue the development there, forgetting 8.14)

Best, Damien

YaZko commented 2 years ago

Perfect, thanks a lot @damien-pous !

damien-pous commented 2 years ago

v1.5 released for coq 8.15 !