O(n) doesn't pass, you need better. If you're saying that the reference solution is O(n), yes, it's a problem and explains the huge variability in the time execution

=> ?

Sorry it has been a long time since I last compiled by myself with ocamlc. Indeed, your solution worked but, with ocamlc, there is a need to add the -I option so that it knows what directory it should use. The line is now:
CWCompileAndRun "fibo.mli" "fibo.ml" Options "-I /opt/coq/default/lib/num /opt/coq/default/lib/num/nums.cma -w -8" Driver "

Honestly, in my opinion, it is almost always simpler to use modern tools like opam/dune when working with OCaml. I guess you were not able to do that because Opam is broken on Debian stable (I don't know it it is still broken actually ?).
Anyway, thank you for your help.
I republished and marked this issue as solved.

CWCompileAndRun "fibo.mli" "fibo.ml" Options "-w -8 /opt/coq/default/lib/num/nums.cma"

might work.

Changing compile_and_run to use ocamlfind and specifying -package num option would be better.

num is already installed because it's required by coq. nums.cma is at /opt/coq/default/lib/num/nums.cma.

Maybe ocamlc needs some flags because num is no longer included in core?

if run_system_command ~err_msg:"Compilation failed" ([ocaml_compiler; options] @ files @ [driver_file]) then begin

https://github.com/codewars/coq_codewars/blob/51a7efe1f7071f94980cc35466f656d9f4370624/src/coq_cw.ml#L168

I managed to make the Coq proof ok (not deployed) for now but I still get some OCaml error. It seems that the nums.cma file is not available:

File "fibo.ml", line 16, characters 16-31:
16 |   type coq_Ze = Big_int.big_int
                     ^^^^^^^^^^^^^^^
Error: Unbound module Big_int
Running: ocamlc nums.cma -w -8 fibo.ml driver.ml

I think maybe it is necessary to install the library num for this new ocamlc ? I hope it could be handled by this command (if you use opam the package manager of ocaml):
opam install num

Most likely, this comes from the way my solution is written (the behavior of some tactics changed between 8.11 and 8.12): I can modify this when I have time.
Thank you for your help.

I just deployed the fix for ocamlc missing, but it's now failing with:

The reference H was not found in the current environment.
File "./Solution.v", line 57, characters 2-12

Yeah, I use multi stage build for Coq image and I had to install ocaml on the final image.
I'll let you know when the fix is deployed.

I probably broke it. I avoided compiling OCaml through OPAM this time.
Looks like there's ocaml but not ocamlc in PATH.

Ah, I see, I'll ping @monadius about it

I looked it up a little bit. There seems to be a problem with the CWCompileAndRun command with Coq8.12. I get the following error: "ocamlc not found".
The test for the plugin in coq_codewars repository (coq plugin) seems to still be working well with Coq 8.12.
I cannot solve this CWCompileAndRun problem on my own (but I can help by providing a solution compatible with Coq 8.12).

This Kata is not compatible with Coq 8.12 as of 08/10/2020

I agree with the statement of ipergenitsa above. Perhaps, for Coq and other theorem proving tools, it would be a good idea to differentiate between different aspects of the katas complexity (with a tag ?):

• Program and prove: the main difficulty is to write and prove a program
• Mathematics: the main difficulty is to find the proof in theoretical maths (I mean that translating it into Coq is easy but the reasonning is hard)
• Logicians and tricks of Coq: the main difficulty is to know the very last features of the tool and the exact logic it relies on.

I think this particular problem would fall into the second category meaning that it is significantly harder for someone with a small background in mathematics. I personally struggled with problems of the third category (for example one using the very new feature of polymorphic universes in Coq).
Note that I may have missed the relevant tags and the respective meaning of 8kyu/7kyu etc (pointers are welcome ;) )