Ali Caglayan

``` ./configure # configure script make dunestrap # generate coq rules dune build -p coq-core,coq-stdlib,coq # build coq packages in release mode dune install coq-core coq-stdlib coq $args # install...

As a minimal, you will need to pass `-coqlib` (or use env var `COQLIB`) that points to a directory containing `theories/Init/Prelude.vo`. Doesn't have to be the real thing, just needs...

@JasonGross Can you provide some more information about how you ran into this? AFAICT this only happens if `./configure` never gets run or `theories/Init/Prelude.vo` cannot be found. Both of which...

@ejgallego Could you open an issue detailing your ideas then? I also had a look at this today, but I concluded that the issue stems from more fundamental design flaws...

>forbid calling Env.init more than once per execution, once you get the env, pass it around to users. This is in effect, how it works today. If you call Env.Init...

@ejgallego I tried it and building the main library didn't trigger anything.

I apologise for my information-dense reply. Let me try to clear a few things up. Firstly, a quick comment: `make -f Makefile.dune` is unneeded now. Due to the work in...

Have you considered pinning your version of dune? Something like ``` opam pin add dune.2.9.0 ``` That will stop it from being upgraded in general. opam will complain if there...

@RalfJung If you are doing this in your CI, are you using the OCaml Github action? There is a way to enable Dune cache for that, which will reduce build...

Here is how to debug: ```coq Require Import Setoid. Require Import Morphisms. (* for Equivalence *) Definition equ {T} {e} `(Equivalence T e) := e. Notation "f == g" :=...