[Agda-dev] Mysteries of the GHC recompilation checker

[Ulf Norell]

Yes, happens for me too. Same OS/ghc version.

Googling turns up this commit

https://gitlab.haskell.org/ghc/ghc/-/commit/bd5ee887a46a4601b08d4e3a8316262a262eb225

There's a `traceHiDiffs` call that actually shows (one of) the missing
dependencies. Compiling with
-ddump-hi-diffs gives (among a bazillion lines of output):

...
missing old home dependency ‘Agda.Syntax.Abstract.Name’
[ 94 of 392] Compiling Agda.Compiler.Builtin[boot] (
src/full/Agda/Compiler/Builtin.hs-boot,
dist-2.6.2-ghc-8.10.2/build/Agda/Compiler/Builtin.o-boot,
dist-2.6.2-ghc-8.10.2/build/Agda/Compiler/Builtin.dy
n_o ) [missing old dependency]
...
missing old home dependency ‘Agda.TypeChecking.Monad.Debug’
[190 of 392] Compiling Agda.TypeChecking.Pretty.Call[boot] (
src/full/Agda/TypeChecking/Pretty/Call.hs-boot,
dist-2.6.2-ghc-8.10.2/build/Agda/TypeChecking/Pretty/Call.o-boot,
dist-2.6.2-ghc-8.10.2/build/
Agda/TypeChecking/Pretty/Call.dyn_o ) [missing old dependency]
...
missing old home dependency ‘Agda.Interaction.Highlighting.Precise’
[201 of 392] Compiling Agda.Interaction.Base (
src/full/Agda/Interaction/Base.hs,
dist-2.6.2-ghc-8.10.2/build/Agda/Interaction/Base.o,
dist-2.6.2-ghc-8.10.2/build/Agda/Interaction/Base.dyn_o ) [missing o
ld dependency]
...
missing old home dependency ‘Agda.Syntax.Internal.Defs’
[350 of 392] Compiling Agda.TypeChecking.Rules.Builtin (
src/full/Agda/TypeChecking/Rules/Builtin.hs,
dist-2.6.2-ghc-8.10.2/build/Agda/TypeChecking/Rules/Builtin.o,
dist-2.6.2-ghc-8.10.2/build/Agda/TypeChecking/Rules/Builtin.dyn_o )
[missing old dependency]
...

Not sure what it all means though...

/ Ulf

On Wed, Oct 28, 2020 at 10:56 AM Andreas Abel <abela at chalmers.se> wrote:

> Do you also see the "missing old dependency" for exactly two files when
> you recompile Agda?  (Mac, GHC 8.10.2)
>
> [201 of 386] Compiling Agda.Interaction.Base (
> src/full/Agda/Interaction/Base.hs,
> dist-2.6.2-ghc-8.10.2/build/Agda/Interaction/Base.o,
> dist-2.6.2-ghc-8.10.2/build/Agda/Interaction/Base.dyn_o ) [missing old
> dependency]
>
> [349 of 386] Compiling Agda.TypeChecking.Rules.Builtin (
> src/full/Agda/TypeChecking/Rules/Builtin.hs,
> dist-2.6.2-ghc-8.10.2/build/Agda/TypeChecking/Rules/Builtin.o,
> dist-2.6.2-ghc-8.10.2/build/Agda/TypeChecking/Rules/Builtin.dyn_o )
> [missing old dependency]
>
> Agda.Interaction.Base and Agda.TypeChecking.Rules.Builtin are always
> recompiled on my machine.  Luckily, this is not infective, files
> depending on these are not recompiled.
>
> Any explanation for this phenomenon?
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www.cse.chalmers.se/~abela/
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda-dev/attachments/20201102/91fbc4ab/attachment.html>