I am trying to make local builds of ci projects and I get error messages regarding modules for different projects with ml code:
make ci-equations
gives Error: Unbound module EConstr
make ci-rewriter
gives Error: Unbound module Names
Any idea what I should do?
how did you build coq? (legacy build or pure dune build?)
does _build_vo exist (as a subfolder of the coq repo root)?
I tried with a fresh clone from github and then:
./configure -profile devel
make
make ci-XXX
that's legacy build, I think it's broken for the ci plugins
try
git clean -xffd
dune build
make -f Makefile.dune ci-xxx
Gaëtan Gilbert said:
that's legacy build, I think it's broken for the ci plugins
It was not broken originally, but I dunno these days
OK thanks, let me try with dune (I have to learn more about it, I am not familiar with dune).
There is probably some documentation update to be done: https://github.com/coq/coq/tree/master/dev/ci/user-overlays
we do
export OCAMLPATH="$PWD/_build_vo/default/lib/:$OCAMLPATH"
export COQBIN="$PWD/_build_vo/default/bin"
export COQLIB="$PWD/_build_vo/default/lib/coq"
export COQCORELIB="$PWD/_build_vo/default/lib/coq-core"
but _build_vo only has kernel tools and plugins
so ocaml can't find econstr in engine etc
main problem is we test that the legacy build can build, install and that the installed result can be used
but we don't test the non-install dev workflow
Olivier Laurent has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC