search

smtcoq / smtcoq-api

An API to interact with SMTCoq
Other
2 stars 1 forks source link

Smtcoq_plugin not found #1

Closed acorrenson closed 1 year ago

acorrenson commented 1 year ago

After installing ocaml 4.10 in a local switch and installing smtcoq 2.0+8.11 (in the same local switch), I still can't compile smtcoq API. make return the following message :

coq_makefile -f _CoqProject -o Makefile
CAMLOPT -c -for-pack Smtcoq_api_plugin api.ml
File "api.ml", line 13, characters 11-24:
13 | module S = Smtcoq_plugin
                ^^^^^^^^^^^^^
Error: Unbound module Smtcoq_plugin
make[1]: *** [api.cmx] Error 2
make: *** [all] Error 2
ckeller commented 1 year ago

I started a port for Coq-8.13 in this branch. It does not compile yet but I will try to finish it as quickly as possible.

ckeller commented 1 year ago

The port was actually easy :-) The branch coq-8.13 is now the default branch, and the branch coq-8.11 will not be maintained.

acorrenson commented 1 year ago

Wow that was fast... Thanks a lot @ckeller ! the problem seems to be solved ^^