Stream: Coq users

Topic: Building Coq from source

view this post on Zulip Clément Pit-Claudel (Oct 05 2021 at 18:33):

Is there a secret trick to run Coq from source these days? Starting from a clean checkout I did ./configure -profile devel then make and make install, but I can't figure out how to invoke the newly built coq binary:

$ echo "Require Import Ltac2.Ltac2." | /build/coq/master/bin/coqtop
Welcome to Coq 8.15+alpha

Coq < Toplevel input, characters 0-27:
> Require Import Ltac2.Ltac2.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error:
File not found on loadpath : ltac2_plugin.cmxs
Loadpath: /tmp/test/:/build/coq/master/_build_vo/default/lib/coq/user-contrib/Ltac2:/build/coq/master/_build/default/plugins/ring:/build/coq/master/_build/default/plugins/btauto:/build/coq/master/_build/default/plugins/ssrsearch:/build/coq/master/_build/default/plugins/ssr:/build/coq/master/_build/default/plugins/nsatz:/build/coq/master/_build/default/plugins/syntax:/build/coq/master/_build/default/plugins/extraction:/build/coq/master/_build/default/plugins/ltac:/build/coq/master/_build/default/plugins/funind:/build/coq/master/_build/default/plugins/cc:/build/coq/master/_build/default/plugins/rtauto:/build/coq/master/_build/default/plugins/micromega:/build/coq/master/_build/default/plugins/derive:/build/coq/master/_build/default/plugins/firstorder:/build/coq/master/_build/default/plugins/ssrmatching

I tried to use the binaries in _build_vo, too:

COQBIN=/build/coq/master/_build_vo/default/bin/  \
COQLIB=/build/coq/master/_build_vo/default/lib/coq/ \
make

But I get the same error:

Error:
File not found on loadpath : ltac2_plugin.cmxs
Loadpath: /tmp/test:/build/coq/master/_build_vo/default/lib/coq/user-contrib/Ltac2:/build/coq/master/_build/default/plugins/ring:/build/coq/master/_build/default/plugins/btauto:/build/coq/master/_build/default/plugins/ssrsearch:/build/coq/master/_build/default/plugins/ssr:/build/coq/master/_build/default/plugins/nsatz:/build/coq/master/_build/default/plugins/syntax:/build/coq/master/_build/default/plugins/extraction:/build/coq/master/_build/default/plugins/ltac:/build/coq/master/_build/default/plugins/funind:/build/coq/master/_build/default/plugins/cc:/build/coq/master/_build/default/plugins/rtauto:/build/coq/master/_build/default/plugins/micromega:/build/coq/master/_build/default/plugins/derive:/build/coq/master/_build/default/plugins/firstorder:/build/coq/master/_build/default/plugins/ssrmatching

view this post on Zulip Emilio Jesús Gallego Arias (Oct 05 2021 at 18:45):

Profile devel is not compatible with install

view this post on Zulip Emilio Jesús Gallego Arias (Oct 05 2021 at 18:46):

look at the paths, Coq is expecting plugins in /build/coq/vm_change/

view this post on Zulip Emilio Jesús Gallego Arias (Oct 05 2021 at 18:46):

set -prefix if you mean to install Coq

view this post on Zulip Emilio Jesús Gallego Arias (Oct 05 2021 at 18:47):

otherwise -profile devel will instruct Coq to search for the plugins in the build dir, as you can see from the debug info

view this post on Zulip Clément Pit-Claudel (Oct 05 2021 at 19:58):

Sorry for the vm_change thing; it was a typo in my description of the issue.

Concretely, what do I actually need to do to be able to run Coq built from source? (Which coqc binary should I use, and how should I invoke it?)

I guess what I'm saying is that on my machine this doesn't work:

cd tmp
git clone --depth 1 git@github.com:coq/coq.git
cd coq
./configure -profile devel
make
echo "Require Import Ltac2.Ltac2." | bin/coqtop

$ echo "Require Import Ltac2.Ltac2." | bin/coqtop
Welcome to Coq 8.15+alpha

Coq < Toplevel input, characters 0-27:
> Require Import Ltac2.Ltac2.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error:
File not found on loadpath : ltac2_plugin.cmxs
Loadpath: /tmp/coq:/tmp/coq/_build_vo/default/lib/coq/user-contrib/Ltac2:/tmp/coq/_build/default/plugins/btauto:/tmp/coq/_build/default/plugins/cc:/tmp/coq/_build/default/plugins/derive:/tmp/coq/_build/default/plugins/extraction:/tmp/coq/_build/default/plugins/firstorder:/tmp/coq/_build/default/plugins/funind:/tmp/coq/_build/default/plugins/ltac:/tmp/coq/_build/default/plugins/micromega:/tmp/coq/_build/default/plugins/nsatz:/tmp/coq/_build/default/plugins/ring:/tmp/coq/_build/default/plugins/rtauto:/tmp/coq/_build/default/plugins/ssr:/tmp/coq/_build/default/plugins/ssrmatching:/tmp/coq/_build/default/plugins/ssrsearch:/tmp/coq/_build/default/plugins/syntax

Coq <

view this post on Zulip Gaëtan Gilbert (Oct 05 2021 at 20:24):

this works:

view this post on Zulip Gaëtan Gilbert (Oct 05 2021 at 20:25):

I've completely lost track of how configure devel works so can't help if you don't want pure dune build

view this post on Zulip Emilio Jesús Gallego Arias (Oct 05 2021 at 21:39):

Indeed, that's a bug in the make compat layer, sorry @Clément Pit-Claudel , the Ltac2 directory is missing

view this post on Zulip Clément Pit-Claudel (Oct 05 2021 at 21:39):

Thanks both, I don't care for make specifically, so this is perfect.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 05 2021 at 21:44):

This problem is specific to Ltac2, but indeed it is a bug worth reporting; you can also workaround it by calling ./bin/coqtop -I _build/default/user-contrib/Ltac2 , seems at some point we confused the .vo with the .cmxs path in the compat layer, but only for user-contrib

view this post on Zulip Emilio Jesús Gallego Arias (Oct 05 2021 at 21:44):

The test suite doesn't catch this because we setup things specifically for it

view this post on Zulip sameer gupta (Oct 05 2021 at 22:06):

I tried that on Gentoo, 32 bit arch. Installation kept failing

Last updated: Sep 23 2023 at 07:01 UTC