fix(coq): make loading of theories in scope lazier

[Alizter]

We make the loading of theories even lazier in scope.ml. This required refactoring the coq db into a Memo.Lazy.t. I'm open to a better way of doing this but this at least fixes the bug observed in #7747 and #7748.

I added a test case for #7747 and showed that this patch fixes it also.

This PR fixes the following issues, however they will be closed on a new run of the opam ci:

• regression: coq-stdlib.8.17.0 #7747
• regression: coq-serapi.8.13.0+0.13.1 #7748

[ejgallego]

Thanks a lot for the quick fix @Alizter , code looks good to me, and indeed the new type seems like the right one.

Sorry for the oversight in the initial implementation.

[ejgallego]

fixes #7747

should also fix the other one, tho your previous PR did also fix that one, so maybe we can mark both PRs as fixing that bug.

[Alizter]

Actually, I will let @emillon close those since he will do another opam build.

[ejgallego]

Actually, I will let @emillon close those since he will do another opam build.

Changelog / PRs description should reflect bugs numbers tho, right?

[Alizter]

I'll mention them in the PR description but we don't need a changelog since we are fixing a bug about a feature we just introduced in this version.

[Alizter]

Looks like there are some changes with the other of execution in the tests, which is expected. However there appears to be a real regression:

--- a/_build/.sandbox/b82be76bda38e00daf81cc2b9fff35ef/default/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/run.t
+++ b/_build/.sandbox/b82be76bda38e00daf81cc2b9fff35ef/default/test/blackbox-tests/test-cases/coq/compose-projects-boot.t/run.t.corrected
@@ -49,7 +49,12 @@ However if this boot library is public Dune will complain
   Error: Cannot have more than one boot theory in scope:
   - Coq at Coq/dune:1
   - Coq at B/Coq/dune:2
-  -> required by _build/default/B/Foo.dune-package
+  -> required by alias B/default
+  Error: Multiple rules generated for
+  _build/install/default/lib/coq/theories/Init/Prelude.v:
+  - Coq/dune:1
+  - B/Coq/dune:2
+  -> required by _build/default/B/Foo.install
   -> required by alias B/all
   -> required by alias B/default
   [1]

and there is an error that is not caught in another test, which I suppose is fine:

--- a/_build/.sandbox/7973c170e23642b9455c3a9c82ae3cfa/default/test/blackbox-tests/test-cases/coq/compose-installed-sub.t/run.t
+++ b/_build/.sandbox/7973c170e23642b9455c3a9c82ae3cfa/default/test/blackbox-tests/test-cases/coq/compose-installed-sub.t/run.t.corrected
@@ -182,10 +182,4 @@ build.
 
   $ dune build --root user
   Entering directory 'user'
-  Error: Coq theory global is defined twice:
-  - theory global in
-    $TESTCASE_ROOT/another-place/lib/coq/user-contrib/global
-  - theory global in
-    $TESTCASE_ROOT/lib/coq/user-contrib/global
   Leaving directory 'user'
-  [1]

[Alizter]

OK so in the first case, the first error is the one we want, however because it is very lazy it is being delayed until rule loading causing it to emit both errors. Ideally we would want only the first error like before. Not sure what the best way to fix this is. Perhaps during rule loading, we can force the database to be constructed.

The second one also looks like a straight up bug.

[ejgallego]

Indeed our current approach to side-effects seems kind of fragile, I do dislike the style where we recover the scope imperatively inside coq_rules helper functions. We should make sure the library resolution is actually memoized, and we are not scanning twice. We resolve now the Coq DB a lot of times per-module, so beware of performance impact.

I would be much more comfortable if we would try to resolve a bit more in the top-level (but again this needs to be done with care)

As for the second error, that's indeed strange, is the test running with the cache enabled? Seems like no rule is triggered and thus no db is built.

Indeed we may have a soundness bug here, as the DB build needs to depend on the contents of the directories that are in COQPATH and user contrib. (Rules should already depend on that)

[Alizter]

I'm not sure there will be a perf impact since the database we are resolving is memod.

The other test does not have caching enabled. (as in behaves the same when explicitly disabling)

@ejgallego I'd appreciate if you could take a look since I am not sure what more I can do here any longer.

[ejgallego]

I'm not sure there will be a perf impact since the database we are resolving is memod.

I meant we should make sure the DB is memoed properly.

The other test does not have caching enabled. (as in behaves the same when explicitly disabling)

I see thanks.

@ejgallego I'd appreciate if you could take a look since I am not sure what more I can do here any longer.

I did have a look and I have no idea what is going on.

I need to leave now, I'd try to put a few printfs in the DB creation code to try to see if the DB code is called and with what paths.

[emillon]

I confirm that at the moment this fixes both regressions on opam. But yeah, don't bother closing these in the PR, I'll do it manually while reviewing the milestone.

[ejgallego]

Thanks @emillon , @Alizter if we don't get the cycles to look at why the DB is being too lazy in this case, IMHO it is fine to open an issue and get 3.8.0 like this, WDTY?

[Alizter]

I don't mind the "multiple rules generated" error message since that is just extra noise essentially, however the other error is a bit more serious. In that case, the duplicate checking in the install directory isn't being carried out, so I would prefer to fix that.

[Alizter]

OK so the missing duplicate checking was actually an incorrectly set up test. Good thing we caught it. I've fixed that and a few other tests now. I will have a look at the multiple rules issue now.

[Alizter]

There isn't much I can do right now about the extra error message. I've decided that since it is quite a niche case about duplicate boot libraries, and the only damage is an extra error message, that it is not really worth fixing at the moment (or even in the future). Therefore I have updated that test.

This should now pass and I am now willing to merge this.

[ejgallego]

Great work, thanks @Alizter . Indeed the duplicate target error is a bit annoying but really a corner case, if someone complains we can fine-tune it easily.