Stream: Coq users

Topic: How to package Coq?

view this post on Zulip Ignat Insarov (Jun 27 2021 at 21:01):

I am trying to package a Coq development so that it can be installed with opam and made visible to Coq. It does not happen.

  1. I can install packages with opam, for example opam install coq-equations works and makes Equations available under ~/.opam/default/lib/coq/user-contrib/Equations.
  2. I tried to follow the official guide. My progress so far is here.
  3. I run opam install . --working-dir to install my development. It succeeds.
  4. Unfortunately the compiled development only becomes available under ~/.opam/default/.opam-switch/build. I expect it to appear under ~/.opam/default/lib as other developments I installed previously.
  5. Apparently Coq does not detect my development. Saying Require Import Example. results in Error: Unable to locate library Example. (While searching for a .vos file.).

What am I doing wrong?

view this post on Zulip Gaëtan Gilbert (Jun 27 2021 at 21:32):

I think you need some -Q or -R to apply to your files for installation to work

view this post on Zulip Gaëtan Gilbert (Jun 27 2021 at 21:32):

ie libraries that have no prefix in their name may have issues

view this post on Zulip Ignat Insarov (Jun 28 2021 at 06:04):

Wohoo! Adding -Q . nice solved the issue.

Last updated: Sep 23 2023 at 14:01 UTC