Stream: Dune devs & users

Topic: Cache poisoning


view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 16:12):

OTOH, I _am_ abusing dune

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 16:13):

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

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 16:33):

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 16:47):

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

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 16:50):

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

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 16:50):

or rather, that was built

view this post on Zulip 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

view this post on Zulip 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 ?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 16:53):

uh

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 16:53):

unfortunately

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 16:53):

That should not be a cache problem

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 16:53):

but more of a loadpath problem

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 16:53):

stuff in very dangerous ways

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 16:54):

ah, there's one local mistake

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 16:59):

so

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

is fine

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 17:21):

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

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 17:21):

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

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 17:22):

which contains dune rules

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 17:23):

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

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 17:24):

Sorry, let me say that better:

view this post on Zulip 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))

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 17:25):

Yeah but how did the stale file got picked

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 17:25):

from global user-contrib ?

view this post on Zulip 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 ...)
)

view this post on Zulip 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.

view this post on Zulip 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
>

view this post on Zulip 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...

view this post on Zulip 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]

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 17:47):

while there's no message about names.vo.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 17:55):

Yeah how to handle this is kinda trikcy

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 17:55):

I don't think the cache is the problem here

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 17:55):

is that the global copy got stale right?

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 17:56):

hm, I don't think so?

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 17:56):

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

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 17:56):

IIUC what you mean

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 17:56):

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 17:57):

empty user-contrib and try again

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 17:57):

can you reproduce then?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 17:57):

at least empty user-contrib/bedrock

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 17:58):

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 17:58):

any restriction I could some with seems too strong

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 17:58):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 18:04):

here it is a bit hard to manage

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 18:04):

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

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 18:05):

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

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 18:05):

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

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 18:06):

(the latter sounds like a hard sell)

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 18:06):

cover in the sense that for any lib in your workspace

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 18:07):

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 18:07):

example bd.{a,b,c}

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 18:07):

3 libs

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 18:07):

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 18:07):

and a <- b <- c

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 18:08):

okay, I don't

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 18:09):

no holes in the middle for me :-)

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 18:09):

but in your example there was a hole right?

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 18:09):

no

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 18:09):

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 18:09):

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 18:10):

oh I see

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 18:10):

here the problem is that bd indeed is bd.*

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 18:10):

so you gotta be careful

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 18:10):

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

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 18:11):

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

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 18:11):

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

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 18:11):

and IIUC it would

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 18:13):

you can still use bd as-is

view this post on Zulip Emilio Jesús Gallego Arias (Oct 04 2020 at 18:13):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 04 2020 at 21:29):

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

view this post on Zulip 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 16 2021 at 07:02 UTC