Stream: Coq devs & plugin devs

Topic: ✔ Problem with local build of ci projects with ml code


view this post on Zulip Olivier Laurent (Nov 09 2021 at 10:51):

I am trying to make local builds of ci projects and I get error messages regarding modules for different projects with ml code:

Any idea what I should do?

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 11:29):

how did you build coq? (legacy build or pure dune build?)
does _build_vo exist (as a subfolder of the coq repo root)?

view this post on Zulip Olivier Laurent (Nov 09 2021 at 11:34):

I tried with a fresh clone from github and then:

./configure -profile devel
make
make ci-XXX

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 11:36):

that's legacy build, I think it's broken for the ci plugins

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 11:36):

try

git clean -xffd
dune build
make -f Makefile.dune ci-xxx

view this post on Zulip Emilio Jesús Gallego Arias (Nov 09 2021 at 11:37):

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

view this post on Zulip Olivier Laurent (Nov 09 2021 at 11:38):

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

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 11:39):

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

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 11:39):

so ocaml can't find econstr in engine etc

view this post on Zulip Gaëtan Gilbert (Nov 09 2021 at 11:44):

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

view this post on Zulip Notification Bot (Nov 09 2021 at 12:03):

Olivier Laurent has marked this topic as resolved.


Last updated: Mar 28 2024 at 14:01 UTC