Stream: Dune devs & users

Topic: Cache poisoning

Paolo Giarrusso (Oct 04 2020 at 16:12):

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

Paolo Giarrusso (Oct 04 2020 at 16:12):

OTOH, I _am_ abusing dune

Paolo Giarrusso (Oct 04 2020 at 16:13):

because I have 2 libraries for logical prefix bedrock., which isn't really supported

Paolo Giarrusso (Oct 04 2020 at 16:33):

Is that the reason, or could there be something else lurking?

Emilio Jesús Gallego Arias (Oct 04 2020 at 16:47):

Where is bedrock.lang.cpp.syntax.names living? It is installed?

Paolo Giarrusso (Oct 04 2020 at 16:50):

hm, there is an installed copy, and one that I'm building

Paolo Giarrusso (Oct 04 2020 at 16:50):

or rather, that was built

Paolo Giarrusso (Oct 04 2020 at 16:51):

$ 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

Emilio Jesús Gallego Arias (Oct 04 2020 at 16:52):

Umm, care to grep in the _build/log for the call building foo.v ?

Emilio Jesús Gallego Arias (Oct 04 2020 at 16:52):

Dune is not yet aware of things in user-contrib so it could indeed pick the global one

Paolo Giarrusso (Oct 04 2020 at 16:52):

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

Paolo Giarrusso (Oct 04 2020 at 16:53):

uh

Emilio Jesús Gallego Arias (Oct 04 2020 at 16:53):

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

Emilio Jesús Gallego Arias (Oct 04 2020 at 16:53):

unfortunately

Emilio Jesús Gallego Arias (Oct 04 2020 at 16:53):

That should not be a cache problem

Emilio Jesús Gallego Arias (Oct 04 2020 at 16:53):

but more of a loadpath problem

Emilio Jesús Gallego Arias (Oct 04 2020 at 16:53):

yeah Coq's loadpath model is giving me many headaches , in particular as how you can shadow stuf

Emilio Jesús Gallego Arias (Oct 04 2020 at 16:53):

stuff in very dangerous ways

Paolo Giarrusso (Oct 04 2020 at 16:54):

ah, there's one local mistake

Paolo Giarrusso (Oct 04 2020 at 16:58):

I haven't put anything in user-contrib explicitly, but . contains cpp2v-core which is a dune project on its own

Paolo Giarrusso (Oct 04 2020 at 16:58):

if I change . to depend on cpp2v-core (which I meant to do, but I had picked the wrong branch), things work better

Paolo Giarrusso (Oct 04 2020 at 16:59):

so

(coq.theory
[...]
   (theories bedrock.lang))

is fine

Emilio Jesús Gallego Arias (Oct 04 2020 at 17:21):

I didn't follow that last part, how is . being picked?

Paolo Giarrusso (Oct 04 2020 at 17:21):

sorry I was unclear, but . is just the current folder throughout the discussion

Paolo Giarrusso (Oct 04 2020 at 17:22):

which contains dune rules

Paolo Giarrusso (Oct 04 2020 at 17:23):

$  find . -name 'dune*'
./cpp2v-core/cpp2v-tests/dune
./cpp2v-core/theories/lang/dune
./theories/dune
./dune-project

Paolo Giarrusso (Oct 04 2020 at 17:23):

and if I add in ./theories/dune a dependency on (theories bedrock.lang), I'm fine

Paolo Giarrusso (Oct 04 2020 at 17:24):

Sorry, let me say that better:

Paolo Giarrusso (Oct 04 2020 at 17:24):

$ cat ./theories/dune
(include_subdirs qualified)

(coq.theory
 (name bedrock)                ; This will determine the toplev
 (package coq-bedrock-auto)
 (flags ...)
 (theories bedrock.lang))

Emilio Jesús Gallego Arias (Oct 04 2020 at 17:25):

Yeah but how did the stale file got picked

Emilio Jesús Gallego Arias (Oct 04 2020 at 17:25):

from global user-contrib ?

Paolo Giarrusso (Oct 04 2020 at 17:25):

and

$ cat ./cpp2v-core/theories/lang/dune
(include_subdirs qualified)
(coq.theory
 (name bedrock.lang)
 (package coq-bedrock-auto)

 (flags ...)
)

Paolo Giarrusso (Oct 04 2020 at 17:29):

sorry again: with these settings, things work correctly. If I drop the (theories bedrock.lang) dependency, things go wrong as I described.

Paolo Giarrusso (Oct 04 2020 at 17:32):

without that dependency, from _build/log, I have the following (where ./theories/auto/uniq.v is a concrete foo):

# 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
>

Paolo Giarrusso (Oct 04 2020 at 17:43):

BTW, why is it using -R? I thought using (include_subdirs qualified) was meant to prevent that...

Paolo Giarrusso (Oct 04 2020 at 17:45):

after 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
>
[1]

Paolo Giarrusso (Oct 04 2020 at 17:47):

while there's no message about names.vo.

Paolo Giarrusso (Oct 04 2020 at 17:48):

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.

Paolo Giarrusso (Oct 04 2020 at 17:49):

$ 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

Paolo Giarrusso (Oct 04 2020 at 17:52):

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)

Paolo Giarrusso (Oct 04 2020 at 17:54):

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

Emilio Jesús Gallego Arias (Oct 04 2020 at 17:55):

Yeah how to handle this is kinda trikcy

Emilio Jesús Gallego Arias (Oct 04 2020 at 17:55):

I don't think the cache is the problem here

Emilio Jesús Gallego Arias (Oct 04 2020 at 17:55):

is that the global copy got stale right?

Emilio Jesús Gallego Arias (Oct 04 2020 at 17:56):

If you switch from local to a global one the rule will be different so the cache shouldn't trigger

Paolo Giarrusso (Oct 04 2020 at 17:56):

hm, I don't think so?

Paolo Giarrusso (Oct 04 2020 at 17:56):

sorry, I don't think the "global copy" is stale

Paolo Giarrusso (Oct 04 2020 at 17:56):

IIUC what you mean

Emilio Jesús Gallego Arias (Oct 04 2020 at 17:56):

it is stale w.r.t. bedrock.auto

Emilio Jesús Gallego Arias (Oct 04 2020 at 17:57):

empty user-contrib and try again

Emilio Jesús Gallego Arias (Oct 04 2020 at 17:57):

can you reproduce then?

Emilio Jesús Gallego Arias (Oct 04 2020 at 17:57):

at least empty user-contrib/bedrock

Emilio Jesús Gallego Arias (Oct 04 2020 at 17:57):

for dune Coq lang 2.0 we won't use any of user-contrib by default, but until then it is tricky to handle

Emilio Jesús Gallego Arias (Oct 04 2020 at 17:58):

in particular due to the ability to overload subsets of module namespaces

Emilio Jesús Gallego Arias (Oct 04 2020 at 17:58):

any restriction I could some with seems too strong

Paolo Giarrusso (Oct 04 2020 at 17:58):

I'm not sure what you mean — the global user-contrib seems consistent

Paolo Giarrusso (Oct 04 2020 at 18:00):

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.

Paolo Giarrusso (Oct 04 2020 at 18:01):

if I empty user-contrib/bedrock, bedrock.lang.cpp.syntax.names will not be found anymore, because it comes from another package.

Paolo Giarrusso (Oct 04 2020 at 18:03):

$ 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

Emilio Jesús Gallego Arias (Oct 04 2020 at 18:03):

Paolo Giarrusso said:

I'm not sure what you mean — the global user-contrib seems consistent

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.

Emilio Jesús Gallego Arias (Oct 04 2020 at 18:04):

I wish I could draw what I think the DAG of the libs looks like :)

Emilio Jesús Gallego Arias (Oct 04 2020 at 18:04):

here it is a bit hard to manage

Paolo Giarrusso (Oct 04 2020 at 18:04):

okay, but would that be fixed if my libs had disjoint prefixes?

Paolo Giarrusso (Oct 04 2020 at 18:05):

I plan to give them bedrock.lang and, say, bedrock.auto

Paolo Giarrusso (Oct 04 2020 at 18:05):

would that work, or would I need bedrockLang and bedrockAuto?

Paolo Giarrusso (Oct 04 2020 at 18:06):

(the latter sounds like a hard sell)

Emilio Jesús Gallego Arias (Oct 04 2020 at 18:06):

As long as you cover in the workspace all the stuff that is globally installed and depends on some overlay yes

Emilio Jesús Gallego Arias (Oct 04 2020 at 18:06):

cover in the sense that for any lib in your workspace

Emilio Jesús Gallego Arias (Oct 04 2020 at 18:07):

the full dependency chain should not cross stuff that is not locally installed

Emilio Jesús Gallego Arias (Oct 04 2020 at 18:07):

example bd.{a,b,c}

Emilio Jesús Gallego Arias (Oct 04 2020 at 18:07):

3 libs

Paolo Giarrusso (Oct 04 2020 at 18:07):

oh, so if I install bedrock.lang globally, I'm screwed?

Emilio Jesús Gallego Arias (Oct 04 2020 at 18:07):

and a <- b <- c

Emilio Jesús Gallego Arias (Oct 04 2020 at 18:08):

so for example if you have c in the workspace, you need b to be too if a is

Emilio Jesús Gallego Arias (Oct 04 2020 at 18:08):

Paolo Giarrusso said:

oh, so if I install bedrock.lang globally, I'm screwed?

not, as long as you don't have chains with "holes" in the middle

Paolo Giarrusso (Oct 04 2020 at 18:08):

okay, I don't

Paolo Giarrusso (Oct 04 2020 at 18:09):

no holes in the middle for me :-)

Emilio Jesús Gallego Arias (Oct 04 2020 at 18:09):

but in your example there was a hole right?

Paolo Giarrusso (Oct 04 2020 at 18:09):

no

Paolo Giarrusso (Oct 04 2020 at 18:09):

I have bd.a and bd, with bd depending on bd.a

Emilio Jesús Gallego Arias (Oct 04 2020 at 18:09):

didn't the missing (theories ...) actually created such hole

Emilio Jesús Gallego Arias (Oct 04 2020 at 18:10):

oh I see

Emilio Jesús Gallego Arias (Oct 04 2020 at 18:10):

here the problem is that bd indeed is bd.*

Emilio Jesús Gallego Arias (Oct 04 2020 at 18:10):

so you gotta be careful

Paolo Giarrusso (Oct 04 2020 at 18:10):

right, that was my conjecture at the outset, because this is unsupported AFAIK

Paolo Giarrusso (Oct 04 2020 at 18:11):

and I tried to say that at the outset and multiple other times

Paolo Giarrusso (Oct 04 2020 at 18:11):

and the hope is that bd.a and bd.b would work

Paolo Giarrusso (Oct 04 2020 at 18:11):

and IIUC it would

Emilio Jesús Gallego Arias (Oct 04 2020 at 18:13):

you can still use bd as-is

Emilio Jesús Gallego Arias (Oct 04 2020 at 18:13):

however you need to be careful indeed as the scope is open

Paolo Giarrusso (Oct 04 2020 at 21:27):

well, the caching is already breaking. for extra fun, I removed the user-contrib stuff, yet the cache was still used.

Paolo Giarrusso (Oct 04 2020 at 21:28):

IOW, the cache for files in bd was still used (where files existed) when bd.a was nowhere to be found.

Paolo Giarrusso (Oct 04 2020 at 21:28):

Hm, actually, I haven’t checked if dune materialized bd.a from the cache without a source file. Either way, not good.

Paolo Giarrusso (Oct 04 2020 at 21:29):

Anyway, let’s stop for now, I’ll just move bd to bd.b.

Paolo Giarrusso (Oct 04 2020 at 21:30):

And clear the cache. And since that should be supported, I’ll ask again if that breaks.

Last updated: Oct 13 2024 at 01:02 UTC