regression: coq-stdlib.8.17.0

[emillon]

Hi,

coq-stdlib.8.17.0 does not build correctly with dune.3.8.0~alpha3, while it did with 3.7.1.
See this build.

#=== ERROR while compiling coq-stdlib.8.17.0 ==================================#
# context              2.2.0~alpha~dev | linux/x86_64 | ocaml-base-compiler.4.14.1 | file:///home/opam/opam-repository
# path                 ~/.opam/4.14/.opam-switch/build/coq-stdlib.8.17.0
# command              ~/.opam/opam-init/hooks/sandbox.sh build ./configure -prefix /home/opam/.opam/4.14 -mandir /home/opam/.opam/4.14/man -libdir /home/opam/.opam/4.14/lib/coq -native-compiler no
# exit-code            1
# env-file             ~/.opam/log/coq-stdlib-7-f87a35.env
# output-file          ~/.opam/log/coq-stdlib-7-f87a35.out
### output ###
# cannot guess a path for Coq libraries; please use -coqlib option or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) If you intend to use Coq without a standard library, the -boot -noinit options must be used.
# Error: Error while running /home/opam/.opam/4.14/bin/coqc --config
# Exit code: 1
# Output:
# 

I bisected that to 98de950 (#7047).

@Alizter can you have a look?

[Alizter]

The issue here is that ./configure is being run with dune exec and coq lang is enabled in the repo, even tho it is useless since coq generates its own rules. This means that somewhere Dune is querying coqc -config even when no coq stanzas are present. This coupled together with the fact that coq is being packaged in a split setup has caused some issues. I need to workout how to fix this. cc @ejgallego who I mentioned this issue to before.

[ejgallego]

This is the same bug than #7748 , dune should not query coqc unless a (coq....) stanza has been found.

Duplicate of #7748

[ejgallego]

Duplicate of #7748

[Alizter]

@ejgallego Are you sure this is the same issue? The other issue was about a value not being found in the config, which was a real bug with coq_config. Here there appears to be a call to coqc -config however this doesn't work without the stdlib.

To fix this, we need to find where we are calling coqc -config and stop doing that.

[Alizter]

The fix for the other issue will not fix this one AFAIK.

[ejgallego]

@ejgallego Are you sure this is the same issue? The other issue was about a value not being found in the config, which was a real bug with coq_config. Here there appears to be a call to coqc -config however this doesn't work without the stdlib.

Yes, I am sure there are the same issue. I don't consider #7748 fixed by #7751

The code for parsing coqc -config was buggy, but the main issue in the first place is that coqc should have never be called in a pure OCaml package.

So while #7751 is a much needed fix, it is only a workaround for #7748 and not a real fix IMO.

[emillon]

Yes, I am sure there are the same issue. I don't consider #7748 fixed by #7751

In terms of release management, #7747 is closed when coq-stdlib builds with dune main, and #7748 is closed when coq-serapi builds with dune main. These are the bugs that I consider blocking the release.

I understand that whether the fix feels "right" is a bit more subjective - in that case feel free to open a new issue regarding the correct design (that might not be fixed by #7751).

[ejgallego]

The culprit is this code:

    let* public_theories =
      let+ coqpaths_of_coq = Coq_path.of_coq_install context
      and+ coqpaths_of_env = Coq_path.of_env context.env in
      let installed_theories =
        Coq_lib.DB.create_from_coqpaths (coqpaths_of_env @ coqpaths_of_coq)
      in
      public_theories coq_stanzas
        ~find_db:(fun _ -> public_libs)
        ~installed_theories
    in

public_theories will return a lazy value, however we aren't lazy enough in the two Coq_path calls.

We should fix this.

It would be nice to patch Coq so indeed coqc -config doesn't crash, but instead prints the configured COQLIB.

[emillon]

main builds correctly now.