agda icon indicating copy to clipboard operation
agda copied to clipboard

Published 20 hours ago • verified publisher icon agda

An infinite loop?

Open nad opened this issue 4 years ago • 22 comments

I just encountered the following message repeatedly, seemingly in an infinite loop:

Failed to validate just-loaded interface: options changed
   Checking Bisimilarity.Weak.Alternative.Classical ([…]).

Before that Agda had checked, or started checking, several files multiple times:

(Lots of output.) 

    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
   Checking Bisimilarity.Equational-reasoning-instances ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
  Checking Bisimilarity.Weak.Alternative ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
  Checking Bisimilarity.Equational-reasoning-instances ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
  Checking Bisimilarity ([…]).
   Checking Bisimilarity.General ([…]).
 Checking Bisimilarity.Weak.Alternative.Equational-reasoning-instances ([…]).
  Checking Bisimilarity ([…]).
   Checking Bisimilarity.General ([…]).
 Checking Bisimilarity.General ([…]).
 Checking Similarity.CCS ([…]).
  Checking Bisimilarity.CCS ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
   Checking Bisimilarity.Equational-reasoning-instances ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
  Checking Bisimilarity ([…]).
   Checking Bisimilarity.General ([…]).
  Checking Similarity ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
 Checking Similarity.Equational-reasoning-instances ([…]).
  Checking Bisimilarity ([…]).
   Checking Bisimilarity.General ([…]).
 Checking Bisimilarity.CCS.Examples.Classical ([…]).
  Checking Bisimilarity.CCS.Classical ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
  Checking Bisimilarity.Equational-reasoning-instances ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
  Checking Bisimilarity ([…]).
   Checking Bisimilarity.General ([…]).
 Checking Bisimilarity.Weak.Alternative ([…]).
  Checking Bisimilarity ([…]).
   Checking Bisimilarity.General ([…]).
 Checking Bisimilarity.Up-to.Counterexamples ([…]).
  Checking Bisimilarity ([…]).
   Checking Bisimilarity.General ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
  Checking Bisimilarity.Equational-reasoning-instances ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
  Checking Bisimilarity ([…]).
   Checking Bisimilarity.General ([…]).
  Checking Expansion ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
 Checking Expansion.Equational-reasoning-instances ([…]).
  Checking Bisimilarity ([…]).
   Checking Bisimilarity.General ([…]).
 Checking Similarity.General ([…]).
 Checking Bisimilarity.Delay-monad ([…]).
  Checking Bisimilarity ([…]).
   Checking Bisimilarity.General ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
   Checking Bisimilarity.Equational-reasoning-instances ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
   Checking Expansion ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
  Checking Expansion.Equational-reasoning-instances ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
  Checking Bisimilarity.Weak ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
  Checking Similarity.Weak ([…]).
   Checking Bisimilarity.Weak ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
    Checking Bisimilarity.Equational-reasoning-instances ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
    Checking Expansion ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
   Checking Expansion.Equational-reasoning-instances ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
   Checking Bisimilarity.Weak ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
   Checking Bisimilarity.Equational-reasoning-instances ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
   Checking Expansion ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
  Checking Bisimilarity.Weak.Equational-reasoning-instances ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
  Checking Bisimilarity ([…]).
   Checking Bisimilarity.General ([…]).
  Checking Expansion ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
  Checking Similarity ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
 Checking Similarity.Weak.Equational-reasoning-instances ([…]).
  Checking Bisimilarity ([…]).
   Checking Bisimilarity.General ([…]).
 Checking Bisimilarity.Weak.Alternative.Up-to.Delay-monad ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
    Checking Bisimilarity.Equational-reasoning-instances ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
   Checking Bisimilarity.Weak.Alternative ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
   Checking Bisimilarity.Equational-reasoning-instances ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
  Checking Bisimilarity.Weak.Alternative.Equational-reasoning-instances ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
 Checking Bisimilarity.CCS.Examples ([…]).
  Checking Bisimilarity.CCS ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
   Checking Bisimilarity.Equational-reasoning-instances ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
  Checking Bisimilarity.General ([…]).
  Checking Similarity.CCS ([…]).
   Checking Bisimilarity.CCS ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
    Checking Bisimilarity.Equational-reasoning-instances ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
  Checking Bisimilarity.Up-to.Counterexamples ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
  Checking Bisimilarity.Delay-monad ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
  Checking Bisimilarity.CCS.Examples ([…]).
   Checking Bisimilarity.CCS ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
    Checking Bisimilarity.Equational-reasoning-instances ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
  Checking Bisimilarity.Comparison ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
    Checking Bisimilarity.Equational-reasoning-instances ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
    Checking Expansion ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
   Checking Expansion.Equational-reasoning-instances ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
   Checking Bisimilarity.Weak ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
   Checking Similarity.Weak ([…]).
    Checking Bisimilarity.Weak ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
      Checking Bisimilarity ([…]).
       Checking Bisimilarity.General ([…]).
     Checking Bisimilarity.Equational-reasoning-instances ([…]).
      Checking Bisimilarity ([…]).
       Checking Bisimilarity.General ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
     Checking Expansion ([…]).
      Checking Bisimilarity ([…]).
       Checking Bisimilarity.General ([…]).
    Checking Expansion.Equational-reasoning-instances ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
    Checking Bisimilarity.Weak ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
    Checking Bisimilarity.Equational-reasoning-instances ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
    Checking Expansion ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
   Checking Bisimilarity.Weak.Equational-reasoning-instances ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
   Checking Expansion ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
  Checking Bisimilarity.Weak.Up-to ([…]).
   Checking Bisimilarity.Weak ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
  Checking Expansion.CCS ([…]).
   Checking Bisimilarity.CCS ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
    Checking Bisimilarity.Equational-reasoning-instances ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
  Checking Bisimilarity.Weak ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
  Checking Up-to.Closure ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
  Checking Bisimilarity.Equational-reasoning-instances ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
  Checking Bisimilarity.CCS ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
   Checking Bisimilarity.Equational-reasoning-instances ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
  Checking Bisimilarity.Weak.Delay-monad ([…]).
   Checking Bisimilarity.Delay-monad ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
  Checking Bisimilarity ([…]).
   Checking Bisimilarity.General ([…]).
  Checking Bisimilarity.Weak.CCS ([…]).
   Checking Bisimilarity.CCS ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
    Checking Bisimilarity.Equational-reasoning-instances ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
  Checking Expansion.Delay-monad ([…]).
   Checking Bisimilarity.Delay-monad ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
  Checking Bisimilarity.CCS.Examples.Natural-numbers ([…]).
   Checking Bisimilarity.CCS ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
    Checking Bisimilarity.Equational-reasoning-instances ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
  Checking Bisimilarity.Up-to.CCS ([…]).
   Checking Bisimilarity.CCS ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
    Checking Bisimilarity.Equational-reasoning-instances ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
   Checking Bisimilarity.Equational-reasoning-instances ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
  Checking Bisimilarity.Up-to ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
  Checking Expansion ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
  Checking Similarity ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
 Checking README.Pointers-to-results-from-the-paper ([…]).
  Checking Bisimilarity ([…]).
   Checking Bisimilarity.General ([…]).
 Checking Bisimilarity.Comparison ([…]).
  Checking Bisimilarity ([…]).
   Checking Bisimilarity.General ([…]).
 Checking Bisimilarity.Weak.Up-to.CCS ([…]).
  Checking Bisimilarity.Weak.CCS ([…]).
   Checking Bisimilarity.CCS ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
    Checking Bisimilarity.Equational-reasoning-instances ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
   Checking Bisimilarity.Equational-reasoning-instances ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
   Checking Expansion ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
  Checking Expansion.Equational-reasoning-instances ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
  Checking Bisimilarity.Weak ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
  Checking Similarity.Weak ([…]).
   Checking Bisimilarity.Weak ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
    Checking Bisimilarity.Equational-reasoning-instances ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
    Checking Expansion ([…]).
     Checking Bisimilarity ([…]).
      Checking Bisimilarity.General ([…]).
   Checking Expansion.Equational-reasoning-instances ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
   Checking Bisimilarity.Weak ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
   Checking Bisimilarity.Equational-reasoning-instances ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
   Checking Expansion ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
  Checking Bisimilarity.Weak.Equational-reasoning-instances ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
  Checking Expansion ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
 Checking Bisimilarity.Weak.Up-to ([…]).
  Checking Bisimilarity.Weak ([…]).
   Checking Bisimilarity ([…]).
    Checking Bisimilarity.General ([…]).
 Checking Expansion.CCS ([…]).
  Checking Bisimilarity.CCS ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
   Checking Bisimilarity.Equational-reasoning-instances ([…]).
    Checking Bisimilarity ([…]).
     Checking Bisimilarity.General ([…]).
 Checking Bisimilarity.Weak ([…]).
  Checking Bisimilarity ([…]).
   Checking Bisimilarity.General ([…]).
 Checking Up-to.Closure ([…]).
  Checking Bisimilarity ([…]).
   Checking Bisimilarity.General ([…]).
 Checking Bisimilarity.Weak.Alternative.Classical ([…]).

I don't know what was going on. I could fix the problem by removing the _build directory.

nad avatar Feb 27 '21 18:02 nad

Before that Agda had checked, or started checking, several files multiple times:

Now I've observed this kind of thing again.

nad avatar Mar 12 '21 17:03 nad

Oh, wow! So chances are that it'll happen again at some point.

Next time, when you get into this state, let's try to capture the state, i.e., your .agda and .agdai files.

I guess the biggest challenge will be to capture a consistent snapshot of the .agdai files while Agda sits in a tight infinite loop overwriting the .agdai files over and over again.

This is on Windows, right? I haven't used a Windows machine in a long time, but maybe the following would work?

  • Create a snap.bat file in the directory that also holds your _build directory. Put the following lines into snap.bat, which rename the _build directory to _snap in a tight loop.

    :forever
rename _build _snap
goto forever

  • Wait until the issue happens again, i.e., until Agda enters the infinite type check loop again.

  • Then run snap.bat. If I correctly remember file system behavior on Windows, then a rename of _build will fail whenever Agda is concurrently accessing one of the .agdai files under _build. That's why we made snap.bat retry the rename in a tight loop.

  • Ultimately, one would hope, one of snap.bat's rename attempts will by chance happen at a time when Agda is busy with type checking per se (as opposed to writing out the interface file), i.e., when Agda isn't accessing any of the .agdai files. Then the rename of _build to _snap will succeed. Now we have a consistent snapshot of _build called _snap.

  • From that point on, snap.bat's rename attempts will always fail, because now _snap already exists. Also, at that point, Agda will probably recreate the _build directory that we just made disappear - which is fine, because we have our _snap.

  • Zip up your work directory, i.e., your .agda files and the _snap directory, and make the Zip archive available for download somewhere.

  • Bonus question: After doing all of the above, let's kill the infinitely looping Agda process, remove the recreated _build directory, and rename _snap back to _build. Then start another type check. Does this make Agda enter the infinite loop again? If so, then - yay! - we even managed to capture the error state in a way that makes the issue easily reproducible.

uncle-betty avatar Mar 14 '21 20:03 uncle-betty

I had already saved a _build directory which exhibits problematic behaviour. If you download issue5245.tgz (which I might remove soon), unpack the files, go into the directory issue5245 and run the following command with Agda 2.6.2-0caec01, then you should see repetitive output (but not Failed to validate just-loaded interface):

agda --library-file libraries --no-default-libraries --library up-to -i up-to up-to/README.agda

nad avatar Mar 16 '21 12:03 nad

Oh, great! Thanks a bunch! I downloaded the file and I am able to reproduce the issue.

uncle-betty avatar Mar 16 '21 16:03 uncle-betty

When I undo the fix for #5161 and then try to reproduce the issue with @nad's .tgz file, Agda aborts pretty early with the following message instead of going into a loop:

/home/tlo/work/issue5245/delay-monad/src/Delay-monad/Bisimilarity.agda:239,45-51
I'm not sure if there should be a case for the constructor E.refl,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
  force y ≟ y′
when checking that the pattern E.refl has type force y ≡ y′

I think that the loop that Agda seemingly goes into isn't actually a loop. To me it looks like Agda just type checks Delay-monad.Bisimilarity over and over again, because a lot of other files import it - directly or transitively. As its interface contains a warning, each import of Delay-monad.Bisimilarity leads to another type check of Delay-monad.Bisimilarity.

When leaving the fix for #5161 intact, my debug build of Agda, for example, takes ~15 minutes to finish type checking @nad's repro. It ultimately finishes with the same error as above.

I'm not sure how this relates to the Failed to validate just-loaded interface issue, though.

uncle-betty avatar Mar 16 '21 21:03 uncle-betty

I think that the type error is due to a recent change to Agda, and that I used an older version of Agda when I got the Failed to validate just-loaded interface message.

nad avatar Mar 17 '21 10:03 nad

I was able to create an MWE for an infinite options changed loop, which I have attached. It works with current master. I don't know, of course, whether this is the same as @nad's infinite options changed loop.

I don't fully understand the details yet. I first need to get a better understanding of pragma option handling for imports.

In any case, the issue seems related to changing options via .agda-lib files. Is this something you did around the time the issue occurred, @nad?

This is the MWE (I'm running it on Linux): repro.tar.gz. Simply run repro.sh inside the repro directory.

uncle-betty avatar Mar 18 '21 20:03 uncle-betty

In any case, the issue seems related to changing options via .agda-lib files. Is this something you did around the time the issue occurred, @nad?

Yes, I think so.

nad avatar Mar 18 '21 22:03 nad

I'd like to propose a fix.

Here's what's going on in the MWE:

  • It contains three libraries - main, a, and b - with modules Main, ModA, and ModB.
  • main depends on a, Main imports ModA.
  • a depends on b, ModA imports ModB.
  • Initially --safe is enabled via the libraries' .agda-lib files. A first type check of Main (and, transitively, ModA and ModB) completes, resulting in three interface files.
  • Then --safe is removed from all the .agda-lib files. ModB.agdai is deleted as well.
  • A second type check of Main results in an infinite options changed loop:
    • Main.agdai gets loaded.
    • ModA.agdai gets loaded, which ends with loadDecodedModule being entered via getStoredInterface.
      • Here, stPragmaOptions is set according to ModA.agdai, i.e., --safe gets enabled.
      • The hashes of ModA's imports are verified and the imports are checked for warnings. This leads to a type-check of ModB and its rejection, because of warnings.
    • The resulting failure of getStoredInterface leads to a type-check of ModA without --safe. Note, however, that stPragmaOptions still contains --safe from loading the original ModA.agdai. This discrepancy is what causes trouble.
    • After the type-check, loadDecodedModule runs again, the discrepancy is discovered, which leads to another type-check of ModA, still with --safe in stPragmaOptions, ... That's the infinite loop.

A fix for current master would be to reset the stPragmaOptions when getStoredInterface fails, as it might already have modified stPragmaOptions:

diff --git a/src/full/Agda/Interaction/Imports.hs b/src/full/Agda/Interaction/Imports.hs
index 08f4c197f..a60778437 100644
--- a/src/full/Agda/Interaction/Imports.hs
+++ b/src/full/Agda/Interaction/Imports.hs
@@ -485,6 +485,7 @@ getInterface x isMain msrc =
 
       let recheck = \reason -> do
             reportSLn "import.iface" 5 $ concat ["  ", prettyShow x, " is not up-to-date because ", reason, "."]
+            setCommandLineOptions . stPersistentOptions . stPersistentState =<< getTC
             case isMain of
               MainInterface _ -> createInterface x file isMain msrc
               NotMainInterface -> createInterfaceIsolated x file msrc

If that makes sense, then I'll be happy to prepare a pull request including a test case. I'm just a little hesitant, because I still don't think I understand the intended invariants for stPragmaOptions in the presence of transitive imports and maybe there's a better fix.

Oh, and I now think that the infinite loop is related to the fix for #5161 as well. Before the fix, we wouldn't have recovered from ModB's warnings. So we wouldn't even have tried to type-check ModA.

uncle-betty avatar Mar 19 '21 21:03 uncle-betty

I think it would be worth it to try out this fix, so could you please make a PR?

jespercockx avatar Mar 31 '21 12:03 jespercockx

Great! Thanks for the guidance, @jespercockx.

uncle-betty avatar Mar 31 '21 14:03 uncle-betty

With Agda version 2.6.2-47702b6-dirty (build yesterday), I am experienced the loop:

...
      Checking Data.Nat.Tactic.RingSolver (/Users/abel/agda-erasure/std-lib/src/Data/Nat/Tactic/RingSolver.agda).
           Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
          Checking Reflection.Argument (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument.agda).
           Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
          Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
         Checking Reflection.Term (/Users/abel/agda-erasure/std-lib/src/Reflection/Term.agda).
           Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
          Checking Reflection.Argument (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument.agda).
           Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
          Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
         Checking Reflection.Argument (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument.agda).
          Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
        Checking Tactic.RingSolver.Core.ReflectionHelp (/Users/abel/agda-erasure/std-lib/src/Tactic/RingSolver/Core/ReflectionHelp.agda).
           Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
          Checking Reflection.Argument (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument.agda).
           Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
          Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
         Checking Reflection.Term (/Users/abel/agda-erasure/std-lib/src/Reflection/Term.agda).
           Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
          Checking Reflection.Argument (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument.agda).
           Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
          Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
         Checking Reflection.Argument (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument.agda).
          Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
         Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
        Checking Reflection.Term (/Users/abel/agda-erasure/std-lib/src/Reflection/Term.agda).
          Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
         Checking Reflection.Argument (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument.agda).
          Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
         Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
        Checking Reflection.Argument (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument.agda).
         Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
           Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
          Checking Reflection.Argument (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument.agda).
           Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
          Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
         Checking Reflection.Term (/Users/abel/agda-erasure/std-lib/src/Reflection/Term.agda).
           Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
          Checking Reflection.Argument (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument.agda).
           Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
          Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
         Checking Reflection.Argument (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument.agda).
          Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
        Checking Data.Nat.Reflection (/Users/abel/agda-erasure/std-lib/src/Data/Nat/Reflection.agda).
           Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
          Checking Reflection.Argument (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument.agda).
           Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
          Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
         Checking Reflection.Term (/Users/abel/agda-erasure/std-lib/src/Reflection/Term.agda).
           Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
          Checking Reflection.Argument (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument.agda).
           Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
       Checking Tactic.RingSolver (/Users/abel/agda-erasure/std-lib/src/Tactic/RingSolver.agda).
           Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
          Checking Reflection.Argument (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument.agda).
           Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
          Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
         Checking Reflection.Term (/Users/abel/agda-erasure/std-lib/src/Reflection/Term.agda).
           Checking Reflection.Argument.Information (/Users/abel/agda-erasure/std-lib/src/Reflection/Argument/Information.agda).
...

andreasabel avatar May 02 '21 17:05 andreasabel

Oh, hey! Surprise!

Hmm. Can you still reproduce it? If so, could you tar up or zip up a copy of your code and your _build directory, and make it available for download somewhere? I'd like to try to reproduce it and to take a shot at this.

uncle-betty avatar May 02 '21 18:05 uncle-betty

Oh, and for how long did you let it loop? I think that it may also be something like the following situation:

  • Suppose that a top-level module A is being type-checked. Suppose that A has a few imports and that a few of these imports in turn import a module B. (The import tree rooted at A will thus have multiple paths from A to B, via different intermediate imports.) Suppose that a type-check of B produces warnings.

  • Suppose that, while type-checking A, Agda transitively gets to B for the first time. Agda type-checks B, which produces warnings, so no interface file gets written for B. However, since the fix for #5161 B's warnings don't abort the overall type-check. Instead, Agda keeps type-checking the rest of A's imports.

  • As multiple of A's imports import B, Agda gets to B a few more times. And each time, B is type-checked. And each time, no interface file is written, because of B's warnings.

So, each time B is reached, it is type-checked anew. Which can look like a loop. In one of the earlier attempts to reproduce the original issue, this behavior made a pretty fast type-check take ~15 minutes. So, this was a case that looked like a loop, but wasn't.

Reflection.Term or Reflection.Argument.Information or Reflection.Argument, for example, might be the equivalent to module B in your log. Does any of them produce warnings when type-checked directly?

uncle-betty avatar May 02 '21 19:05 uncle-betty

I pressed Ctrl-C after maybe a couple hundred lines of Checking Foo with a repeating pattern. I am packing the material which reproduces this, but its more than 300MB, will take while to upload.

In general, I don't think the same file should be checked visited several times during checking a module. So if I see Checking B twice, I consider this a bug. Because that never happened in the olden times, and it is reasonable to expect that the results of checking B are cached.

So, each time B is reached, it is type-checked anew.

Yeah, this is already a bug.

andreasabel avatar May 03 '21 07:05 andreasabel

Material is here: http://www.cse.chalmers.se/~abela/tmp/agda-issue-5245/index.html

andreasabel avatar May 03 '21 08:05 andreasabel

Great! Thanks for the upload. I was able to reproduce the issue.

A bit over 8 minutes after starting the type-check, Agda finished with:

/home/tlo/work/5245/std-lib/src/Reflection/Argument/Information.agda:34,28-29
Agda.Builtin.Reflection.Modality !=< Relevance
when checking that the expression r has type Relevance
Makefile:14: recipe for target 'lab3' failed
make: *** [lab3] Error 42

For some reason, when I looked into this ticket originally, I assumed that this re-check was by design. But now I agree that this is a bug. I didn't mean to imply otherwise. I just meant to say that I believe that we have two distinct bugs at our hands.

(i) One is a bona fide infinite loop, which I think is still fixed. (ii) The other is a needless re-check of modules with warnings, which "just" makes type-checks take exceedingly long. Which is what you encountered.

I suggest that I'll open a separate issue for (ii). Let's maybe not conflate (i) and (ii). We'll need a separate, distinct test case for (ii) anyway and a separate issue number would also be handy for that.

uncle-betty avatar May 03 '21 09:05 uncle-betty

I created an MWE for (ii) and opened a separate issue to track it: #5357. Let's maybe move further discussion over there.

uncle-betty avatar May 03 '21 10:05 uncle-betty 

mkdir fresh
cd fresh
git clone https://github.com/agda/agda-stdlib
(cd agda-stdlib && git checkout v1.7.2)
git clone https://github.com/graded-type-theory/graded-type-theory
cd graded-type-theory
git checkout 8858200068f2c42708bfa9f9879a199fbed99ff0
printf '../agda-stdlib/standard-library.agda-lib\ngraded-type-theory.agda-lib' > libraries
sed -ri 's/--without-K/--cubical-compatible/' graded-type-theory.agda-lib
(sleep 1; sed -ri 's/--cubical-compatible/--without-K/' graded-type-theory.agda-lib) & agda --no-default-libraries --library-file=libraries Graded/Usage.agda

After a while the following message is printed repeatedly (at least for me):

Failed to validate just-loaded interface: options changed
  Checking Tools.Bool ([…]/fresh/graded-type-theory/Tools/Bool.agda).

nad avatar Sep 03 '23 21:09 nad

After a while the following message is printed repeatedly

@nad, does this mean "several times" or did you have to interrupt? I am asking for clarification because both issues were discussed above.

andreasabel avatar Sep 04 '23 12:09 andreasabel

Agda seemed to have gotten stuck in an infinite loop.

nad avatar Sep 05 '23 14:09 nad

I updated the script above:

mkdir fresh
cd fresh
git clone https://github.com/agda/agda-stdlib
(cd agda-stdlib && git checkout b0505d661fbbfecf7ffeae20cc4b48c8ef41e078)
git clone https://github.com/graded-type-theory/graded-type-theory
cd graded-type-theory
git checkout 5a4d9eaf5af978f97142801da220373b78ab572d
printf '../agda-stdlib/standard-library.agda-lib\ngraded-type-theory.agda-lib' > libraries
sed -ri 's/--without-K/--cubical-compatible/' graded-type-theory.agda-lib
(sleep 1; sed -ri 's/--cubical-compatible/--without-K/' graded-type-theory.agda-lib) & agda --no-default-libraries --library-file=libraries Graded/Usage.agda

Failed to validate just-loaded interface: options changed
  Checking Tools.Sum ([…]/fresh/graded-type-theory/Tools/Sum.agda).

nad avatar May 04 '25 19:05 nad