Performance regression #3435
Comments
nad
added
performance
|
What does |
|
Do you have a bisect running? |
For the dependencies, with 2.5.4.2: With 2.6.0-4a5e1dc:
For the final module, with 2.5.4.2: With 2.6.0-4a5e1dc:
|
Not yet, but I plan to. |
|
I've done some investigation and I believe the problem is @jespercockx's lifting of the restriction on unconstrained metas in instance goals. In the example there are a lot of instances in scope and I suspect they are now all attempted instead of waiting for the goal type to be solved. I'm working on a stand-alone test case. |
|
Self-contained test case. Checks more or less instantly on infix -1 finally₂
infixr -2 step-∼
postulate
Transitive : {A B : Set} (P : A → A → Set) (Q : A → B → Set) → Set
step-∼ : ∀ {A B} {P : A → A → Set} {Q : A → B → Set}
⦃ t : Transitive P Q ⦄ x {y z} →
Q y z → P x y → Q x z
Convertible : {A B : Set} (P Q : A → B → Set) → Set
finally₂ : ∀ {A B} {P Q : A → B → Set}
⦃ c : Convertible P Q ⦄ x y →
P x y → Q x y
syntax step-∼ x Qyz Pxy = x ∼⟨ Pxy ⟩ Qyz
syntax finally₂ x y x∼y = x ∼⟨ x∼y ⟩■ y
infix 4 _≈_
postulate
Proc : Set
_≈_ : Proc → Proc → Set
instance
postulate
trans : Transitive _≈_ _≈_
convert : Convertible _≈_ _≈_
module DummyInstances where
postulate
R₁ R₂ R₃ R₄ R₅ : Proc → Proc → Set
postulate
instance
transitive₁₁ : Transitive R₁ R₁
transitive₁₂ : Transitive R₁ R₂
transitive₁₃ : Transitive R₁ R₃
transitive₁₄ : Transitive R₁ R₄
transitive₁₅ : Transitive R₁ R₅
transitive₂₁ : Transitive R₂ R₁
transitive₂₂ : Transitive R₂ R₂
transitive₂₃ : Transitive R₂ R₃
transitive₂₄ : Transitive R₂ R₄
transitive₂₅ : Transitive R₂ R₅
transitive₃₁ : Transitive R₃ R₁
transitive₃₂ : Transitive R₃ R₂
transitive₃₃ : Transitive R₃ R₃
transitive₃₄ : Transitive R₃ R₄
transitive₃₅ : Transitive R₃ R₅
transitive₄₁ : Transitive R₄ R₁
transitive₄₂ : Transitive R₄ R₂
transitive₄₃ : Transitive R₄ R₃
transitive₄₄ : Transitive R₄ R₄
transitive₄₅ : Transitive R₄ R₅
transitive₅₁ : Transitive R₅ R₁
transitive₅₂ : Transitive R₅ R₂
transitive₅₃ : Transitive R₅ R₃
transitive₅₄ : Transitive R₅ R₄
transitive₅₅ : Transitive R₅ R₅
postulate
⊕-comm : ∀ {P Q} → P ≈ Q
P Q : Proc
⊕-cong : P ≈ P
⊕-cong =
P ∼⟨ ⊕-comm ⟩
Q ∼⟨ ⊕-comm ⟩
P ∼⟨ ⊕-comm ⟩
Q ∼⟨ ⊕-comm ⟩
P ∼⟨ ⊕-comm ⟩
Q ∼⟨ ⊕-comm ⟩
P ∼⟨ ⊕-comm ⟩
Q ∼⟨ ⊕-comm ⟩
P ∼⟨ ⊕-comm ⟩
Q ∼⟨ ⊕-comm ⟩■
P |
|
OK, then I won't run a bisection. |
|
In case anyone else wants to do this the following code might be a suitable starting point (the code assumes that the setup described in the OP was performed in $ cat script.hs
#!/usr/bin/env runhaskell
{-# LANGUAGE RecordWildCards #-}
import Control.Monad
import Data.List
import System.Directory
import System.Exit
import System.Timeout
import RunAgda
main :: IO ()
main = do
setCurrentDirectory "regression/up-to"
runAgda [ "--no-default-libraries"
, "--library-file=../libraries"
] $ \(AgdaCommands { .. }) -> do
echoUntilPrompt
loadAndEcho "src/Dependencies.agda"
let mainFile = "src/Bisimilarity/Weak/CCS.agda"
let interface = mainFile ++ "i"
ex <- doesFileExist interface
when ex $ removeFile interface
r <- timeout (70*10^6) $ loadAndEcho mainFile
case r of
Nothing -> do
putStrLn "Timeout!"
exitFailure
Just ss ->
if any ("(agda2-status-action \"Checked\")" `isInfixOf`) ss then
return ()
else
exitWith (ExitFailure 127)
$ agda-bisect --cache --good v2.5.4.2 --bad 4a5e1dc --log log --compiler <ghc-7.10.3> --script ./script.hsNote that this code uses some features of agda-bisect that I pushed just now. |
|
The code also relies on In general I think bisection would be easier if releases were part of the main "trunk" of the commit tree (so that the current HEAD was a descendant of the releases). |
|
I think you might want to use the stand-alone test case rather than the one from the OP. But in this case I think a manual bisect would be faster. I'm quite confident that the unconstrained metas in instance search change is the culprit. |
On closer thought the problem is perhaps rather that the "commit tree" is not a tree but a DAG. I imagine that things would be easier if long-lived branches were rebased before they were incorporated into the main branch.
I dumped my partial work above in order to perhaps save time for future investigations of performance regressions. |
|
PR #3455 fixes the problem, but changed order of constraint solving means a few more sizes need to be given explicitly in the original test case. |
|
I tried this PR. A single experiment gave a slowdown of about 15% for the dependencies. For the final module the slowdown was about 28%. (Note that the code linked above does not quite work using Agda 2.6.0-1b51287. I patched the code and used the same code for both tests.) I noticed that I have compiled 2.5.4.3 using GHC 8.4.4, and Agda 2.6.0-1b51287 using GHC 8.6.3, so changes to GHC could affect the result, even though I suspect that changes to Agda are to blame. Profiling output for the dependencies, with 2.5.4.2: With 2.6.0-1b51287: Profiling output for the final module, with 2.5.4.2: With 2.6.0-1b51287: |
I have some code that type-checks about ten times slower using Agda 2.6.0-4a5e1dc, compared to Agda 2.5.4.2:
The first call to
agdaabove takes about three times longer (with my current setup), and the second call about ten times longer. However, memory usage ("total memory in use") is lower.The text was updated successfully, but these errors were encountered: