Rocq and mathcomp from Homebrew do not work well

Using Rocq
1

I installed Rocq using Homebrew by brew install rocq as Install the Rocq Prover

And I also installed mathcomp by brew install math-comp.

Then, I compile the following file “example.v“ by rocq c example.v, but error occurred.

From mathcomp
     Require Import all_boot.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(* ********************* *)

Definition double_add1 (n:nat) := n * 2 + 1.

Lemma double_add1_odd : forall n, odd (double_add1 n).
Proof. by elim =>[|n]//=->. Qed.

Error message

File "./example.v", line 1, characters 0-43:
Error:
Findlib error: ppx_deriving.runtime not found in:
/usr/local/lib/ocaml/coq/../rocq-runtime/..
/usr/local/lib/ocaml

Is not “ppx_deriving.runtime” included in Rocq or mathcomp from Homebrew?

2

I am not a Homebrew user, but the way rocq-elpi is built seems especially fragile. In particular, did you read the following caveat, which recommends that you set some environment variables and which presumably was displayed by Homebrew during installation? homebrew-core/Formula/r/rocq-elpi.rb at ddb6611f5fccc9b6cf6a6ca6670bb009d84b9fce · Homebrew/homebrew-core · GitHub

3

Thank you for your answer. But I don’t know how to fix it.

In rocq-elpi.rb, line 71, I don’t know actual opt_libexec value in my environment.

In line 76, #{opt_libexec}/lib/findlib.conf is a hint of the path, but I don’t have findlib.conf