8000 An infinite loop? · Issue #5245 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content
An infinite loop? #5245
Open
Open
@nad

Description

@nad

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    interfaceSerialization and loading of interface filestype: bugIssues and pull requests about actual bugsux: optionsIssues relating to Agda's command line options

    Type

    No type

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions

      0