Fix Certicoq Eval and Certicoq Run failing

[jeremyThibault]

Hello,

I've been experimenting with the Certicoq plugin and I ran into some issues when trying to run Certicoq Run and Certicoq Eval, inside Emacs with Proof General.

From CertiCoq.Plugin Require Import CertiCoq.

Definition zero: nat := 0.

CertiCoq Compile zero. (* succeeds! *)

Fail CertiCoq Run zero. (* fails! *)
Fail CertiCoq Eval zero. (* fails! *)

For CertiCoq Run zero, I run into the following error:

error: 'prim_string.h' file not found
    4 | #include <prim_string.h>
      |          ^~~~~~~~~~~~~~~
1 error generated.
Error:
Compiler exited with code 1 while running /usr/bin/gcc -Wno-everything -O2 -fomit-frame-pointer -g -I . -I /Users/jeremy/.opam/certicoq/lib/coq/user-contrib/CertiCoq/Plugin/runtime -c -o ./Zero.zero.o ./Zero.zero.c

After copying prim_string.h inside the lib/coq/user-contrib/CertiCoq/Plugin/runtime directory, CertiCoq Run zero still returns an error about not finding prim_string.o. Compiling prim_string.c manually and copying it into the runtime folder works.

Commit 18a1d55 adds prim_string to the list of targets in the Makefile so that prim_string.h and prim_string.o get properly installed when installing Certicoq.

Even after doing that, I still run into an error when executing CertiCoq Eval zero.:

Debug: Looking up Zero.zero in certicoq_run_functions
Debug: Not found
Debug: Looking for fresh Zero.zero in
Debug: Found Zero.zero
Error: Command
/Users/jeremy/.opam/certicoq/bin/ocamlfind ocamlopt -shared -linkpkg -dontlink str,unix,dynlink,threads,zarith,coq-core,coq-core.plugins.ltac,coq-core.interp -thread -rectypes -package coq-core,coq-core.plugins.ltac,coq-metacoq-template-ocaml,coq-core.interp,coq-core.kernel,coq-core.library -I . -I plugin -o ./Zero.zero.cmxs ./Zero.zero_wrapper.ml /Users/jeremy/.opam/certicoq/lib/coq/user-contrib/CertiCoq/Plugin/runtime/gc_stack.o ./Zero.zero.o /Users/jeremy/.opam/certicoq/lib/coq/user-contrib/CertiCoq/Plugin/runtime/prim_string.o /Users/jeremy/.opam/certicoq/lib/coq/user-contrib/CertiCoq/Plugin/runtime/prim_floats.o /Users/jeremy/.opam/certicoq/lib/coq/user-contrib/CertiCoq/Plugin/runtime/prim_int63.o /Users/jeremy/.opam/certicoq/lib/coq/user-contrib/CertiCoq/Plugin/runtime/coq_ffi.o
exited with code 2.
stdout: 

stderr: File "./Zero.zero_wrapper.ml", line 2, characters 8-54:
2 | let _ = Certicoq_plugin.Certicoq.register_certicoq_run "Zero.zero" "Zero.zero" (Obj.magic zero_zero)
            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound module Certicoq_plugin

(The debug messages are present even though I didn't turn the debug flag on.)

After a bit of experimenting, I managed to make it work by using the following command:

/Users/jeremy/.opam/certicoq/bin/ocamlfind ocamlopt -shared -linkpkg -dontlink str,unix,dynlink,threads,zarith,coq-core,coq-core.plugins.ltac,coq-core.interp,coq-certicoq -thread -rectypes -package coq-core,coq-core.plugins.ltac,coq-metacoq-template-ocaml,coq-core.interp,coq-core.kernel,coq-core.library,coq-certicoq -I . -I plugin -o ./Zero.zero0.cmxs ./Zero.zero0_wrapper.ml /Users/jeremy/.opam/certicoq/lib/coq/user-contrib/CertiCoq/Plugin/runtime/gc_stack.o ./Zero.zero0.o /Users/jeremy/.opam/certicoq/lib/coq/user-contrib/CertiCoq/Plugin/runtime/prim_string.o /Users/jeremy/.opam/certicoq/lib/coq/user-contrib/CertiCoq/Plugin/runtime/prim_floats.o /Users/jeremy/.opam/certicoq/lib/coq/user-contrib/CertiCoq/Plugin/runtime/prim_int63.o /Users/jeremy/.opam/certicoq/lib/coq/user-contrib/CertiCoq/Plugin/runtime/coq_ffi.o

(adding -package coq-certicoq and -dontlink coq-certicoq.)

I've modified the command that is generated by Certicoq Eval in commit 2d93977. This setup works locally on my machine, but I'm not completely sure this is the best way to do this :)

Let me know if I can be of any help!