Skip to content

Experience report on trying to use Dune to build a Coq project. #2042

New issue
New issue
Closed
Closed
Experience report on trying to use Dune to build a Coq project.#2042
Labels
coq
@Zimmi48

Description

@Zimmi48
Zimmi48
opened on Apr 10, 2019
  1. dune init has been introduced in 1.9.0 but obviously it does not support Coq. No problem, it is easy enough to create a dune file based on the examples in the doc.
  2. I add a single dune file, it creates a dune-project file automatically and put the following in it: 
    (lang dune 1.9)
(using coqlib 0.1)
  3. I try to rebuild, Dune says Error: Unknown extension "coqlib".
  4. I remove the "lib" part from dune-project that is an obvious (small) mistake and try to rebuild. Dune says Error: Program ocamlc not found in the tree or in PATH (context: default)
  5. I add ocamlc to my PATH (even if it's a pure Coq project) and try to rebuild. It works 🎉

Metadata

Metadata

Assignees

No one assigned

    Labels

    coq

    Type

    No type

    Projects

    Coq + Dune

    Status

    Done

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions