every now and then, I get
dune's cache in an inconsistent state:
File "./theories/proofmode/cpp/_at_as_Rep.v", line 7, characters 0-50: Error: Compiled library foo (in file /Users/pgiarrusso/git-bedrock/Coq/cpp2v/_build/default/theories/foo.vo) makes inconsistent assumptions over library bedrock.lang.cpp.syntax.names
OTOH, I _am_ abusing dune
because I have 2 libraries for logical prefix
bedrock., which isn't really supported
Is that the reason, or could there be something else lurking?
bedrock.lang.cpp.syntax.names living? It is installed?
hm, there is an installed copy, and one that I'm building
or rather, that was built
$ find . -name names.vo ./_build/install/default/lib/coq/user-contrib/bedrock/lang/cpp/syntax/names.vo ./_build/default/cpp2v-core/theories/lang/cpp/syntax/names.vo
Umm, care to grep in the
_build/log for the call building foo.v ?
Dune is not yet aware of things in
user-contrib so it could indeed pick the global one
IIRC from last time, dune clean doesn't help because of the cache, and shrinking the cache to 0 with
dune cache --trimmed-size=0 doesn't help either
tho that would be weird if the rules for foo are OK, but now that you mention it there is some issue with ordering of loadpaths
That should not be a cache problem
but more of a loadpath problem
yeah Coq's loadpath model is giving me many headaches , in particular as how you can shadow stuf
stuff in very dangerous ways
ah, there's one local mistake
I haven't put anything in user-contrib explicitly, but
cpp2v-core which is a dune project on its own
if I change
. to depend on
cpp2v-core (which I meant to do, but I had picked the wrong branch), things work better
(coq.theory [...] (theories bedrock.lang))
I didn't follow that last part, how is
. being picked?
sorry I was unclear, but
. is just the current folder throughout the discussion
which contains dune rules
$ find . -name 'dune*' ./cpp2v-core/cpp2v-tests/dune ./cpp2v-core/theories/lang/dune ./theories/dune ./dune-project
and if I add in
./theories/dune a dependency on
(theories bedrock.lang), I'm fine
Sorry, let me say that better:
$ cat ./theories/dune (include_subdirs qualified) (coq.theory (name bedrock) ; This will determine the toplev (package coq-bedrock-auto) (flags ...) (theories bedrock.lang))
Yeah but how did the stale file got picked
$ cat ./cpp2v-core/theories/lang/dune (include_subdirs qualified) (coq.theory (name bedrock.lang) (package coq-bedrock-auto) (flags ...) )
sorry again: with these settings, things work correctly. If I drop the
(theories bedrock.lang) dependency, things go wrong as I described.
without that dependency, from _build/log, I have the following (where
./theories/auto/uniq.v is a concrete
# cache miss for 85f9cc8ca43d6036b8d1dddc21dcd052: no cached file $ (cd _build/default && /Users/pgiarrusso/.opam/iris-3.3-coq-8.11.2/bin/coqc -w -convert_concl_no_check -w -ambiguous-paths -R theories bedrock theories/auto/uniq.v) > File "./theories/auto/uniq.v", line 7, characters 0-28: > Error: > Compiled library bedrock.auto (in file /Users/pgiarrusso/git-bedrock/Coq/cpp2v/_build/default/theories/auto.vo) makes inconsistent assumptions over library bedrock.lang.cpp.syntax.names >
BTW, why is it using
-R? I thought using
(include_subdirs qualified) was meant to prevent that...
dune clean, the log ends in:
# cache hit for 4a80cc1ecb1d1b3299221233f7a89cac # retrieve _build/default/theories/auto.vo from cache # cache miss for 85f9cc8ca43d6036b8d1dddc21dcd052: no cached file $ (cd _build/default && /Users/pgiarrusso/.opam/iris-3.3-coq-8.11.2/bin/coqc -w -convert_concl_no_check -w -ambiguous-paths -R theories bedrock theories/auto/uniq.v) > File "./theories/auto/uniq.v", line 7, characters 0-28: > Error: > Compiled library bedrock.auto (in file /Users/pgiarrusso/git-bedrock/Coq/cpp2v/_build/default/theories/auto.vo) makes inconsistent assumptions over library bedrock.lang.cpp.syntax.names > 
while there's no message about
ah. For extra fun, I can reproduce all this even if I move the local
cpp2v-core out of the way, and just use the globally installed version.
$ find . -name 'names.vo' $ find . -name 'names.v' $ dune build ./theories/auto/uniq.vo File "./theories/auto/uniq.v", line 7, characters 0-28: Error: Compiled library bedrock.auto (in file /Users/pgiarrusso/git-bedrock/Coq/cpp2v/_build/default/theories/auto.vo) makes inconsistent assumptions over library bedrock.lang.cpp.syntax.names
in which case, the only explanation seems that dune's picking a stale
uniq.vo file from the cache, because it's not tracking the contents of the global
user-contrib? Hopefully, that's because the file is under
bedrock.* and I'm building a coq.theory with path
bedrock, which is outside the specs and violates dune's closed-world assumption (which you mentioned other times)
and to be sure, I'm happy to switch to disjoint logical paths and wipe my cache — I only fear that'd destroy data for a valid bug report @Emilio Jesús Gallego Arias
Yeah how to handle this is kinda trikcy
I don't think the cache is the problem here
is that the global copy got stale right?
If you switch from local to a global one the rule will be different so the cache shouldn't trigger
hm, I don't think so?
sorry, I don't think the "global copy" is stale
IIUC what you mean
it is stale w.r.t.
user-contrib and try again
can you reproduce then?
at least empty
for dune Coq lang 2.0 we won't use any of user-contrib by default, but until then it is tricky to handle
in particular due to the ability to overload subsets of module namespaces
any restriction I could some with seems too strong
I'm not sure what you mean — the global
user-contrib seems consistent
indeed, I can load all the offenders just fine elsewhere:
Require Import bedrock.auto. Require Import bedrock.auto.uniq. Require Import bedrock.lang.cpp.syntax.names.
if I empty
bedrock.lang.cpp.syntax.names will not be found anymore, because it comes from another package.
$ mv /Users/pgiarrusso/.opam/iris-3.3-coq-8.11.2/lib/coq/user-contrib/bedrock ../user-contrib-bedrock $ dune build ./theories/auto/uniq.vo File "./theories/auto/uniq.v", line 7, characters 0-28: Error: Cannot find library bedrock.IrisBridge in loadpath
Paolo Giarrusso said:
I'm not sure what you mean — the global
It is tricky as if you add your theory
bedrock.foo, then suddently a sub-slice of the libs in
user-contrib have been replaced, however the stuff in
user-contribdepending on that sub-slice will not be compiled back. Thus we are left with an inconsistent state due to this weird ability of Coq to replace sub-namespaces.
I wish I could draw what I think the DAG of the libs looks like :)
here it is a bit hard to manage
okay, but would that be fixed if my libs had disjoint prefixes?
I plan to give them
bedrock.lang and, say,
would that work, or would I need
(the latter sounds like a hard sell)
As long as you cover in the workspace all the stuff that is globally installed and depends on some overlay yes
cover in the sense that for any lib in your workspace
the full dependency chain should not cross stuff that is not locally installed
oh, so if I install
bedrock.lang globally, I'm screwed?
a <- b <- c
so for example if you have
c in the workspace, you need
b to be too if
Paolo Giarrusso said:
oh, so if I install
bedrock.langglobally, I'm screwed?
not, as long as you don't have chains with "holes" in the middle
okay, I don't
no holes in the middle for me :-)
but in your example there was a hole right?
bd depending on
didn't the missing
(theories ...) actually created such hole
oh I see
here the problem is that
bd indeed is
so you gotta be careful
right, that was my conjecture at the outset, because this is unsupported AFAIK
and I tried to say that at the outset and multiple other times
and the hope is that
bd.b would work
and IIUC it would
you can still use
however you need to be careful indeed as the scope is open
well, the caching is already breaking. for extra fun, I removed the user-contrib stuff, yet the cache was still used.
IOW, the cache for files in bd was still used (where files existed) when bd.a was nowhere to be found.
Hm, actually, I haven’t checked if dune materialized bd.a from the cache without a source file. Either way, not good.
Anyway, let’s stop for now, I’ll just move bd to bd.b.
And clear the cache. And since that should be supported, I’ll ask again if that breaks.
Last updated: Oct 16 2021 at 07:02 UTC