Speed up morphism search of setoid-rewrite

mattam82 commented 3 years ago

This is another patch that greatly speeds up setoid_rewrite (removing some of the existing logic to handle pointwise relations, that are now better done by the Coq PR). Hopefully it is also backwards compatible, otherwise, I'll make an overlay for coq/coq#13969

cpitclaudel commented 3 years ago

Magic! Do you have tips written somewhere about how you came up with these specific optimizations?

mattam82 commented 3 years ago

You have to know a bit the inner workings of the tactic but in general:

add Params declarations for polymorphic constants and even general ones that have a lot of arguments: this allows the "partial application" rule to fire just once (it handles finding Proper R (f x) from a user-given Proper (R' ==> R) f instance.
Do not put a Hint Extern 0 => solve [apply reflexivity] : typeclass_instance :) that can apply to goals you wouldn't expect.
Also, using subrelation R S instances instead of rolling ones own logic to infer Proper (pointwise_relation R) (eq ==> R) f seems to help here.

In general to debug I just look at the trace, looking for a subgoal that gets a lot of tries (e.g. if 2.1.* appears a lot then probably the problem lies in this subgoal, either it should not be generated or there is a weird choice being made there). Another indication is when you backtrack to 2.1 after solving 4.2, it means we went with a wrong choice at the beginning, so we should look at the 2.1 goal to undestand the problem.

cpitclaudel commented 3 years ago

Thanks!

mattam82 commented 3 years ago

It looks like it will be backwards compatible, yay!

mattam82 commented 3 years ago

If I read this right, we just gained 50seconds: With this PR:

-----------------------------------------------------------------------------------------------------
10m01.68s | 932696 ko | Total Time / Peak Mem                                                        
-----------------------------------------------------------------------------------------------------
 0m33.87s | 660612 ko | Parsers/GenericRecognizerMin                                                 
 0m31.71s | 680196 ko | Parsers/Refinement/PossibleTerminalsSets                                     
 0m25.96s | 713960 ko | Parsers/ParserFromParserADT                                                  
 0m25.96s | 713960 ko | ─abstract                                                                    
 0m25.34s | 932696 ko | Parsers/BooleanRecognizerOptimized                                           
 0m20.77s | 824976 ko | Parsers/GenericRecognizerOptimized                                           
 0m18.51s | 539532 ko | Common/FMapExtensions                                                        
 0m18.17s | 841848 ko | Parsers/BooleanRecognizerOptimizedReflectiveCorrectness                      
 0m16.65s | 567316 ko | Parsers/SplitterFromParserADT                                                
 0m14.15s | 476752 ko | Parsers/Refinement/BinOpBrackets/MakeBinOpTable                              
 0m11.89s | 789396 ko | Parsers/Reflective/LogicalRelations                                          
 0m10.87s | 582312 ko | Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflective                  
 0m10.55s | 514676 ko | Common/List/ListFacts                                                        
 0m07.48s | 459312 ko | Parsers/StringLike/FirstCharSuchThat                                         
 0m07.35s | 496656 ko | Parsers/ContextFreeGrammar/Fix/ProdAbstractInterpretationDefinitions         
 0m06.90s | 500596 ko | Parsers/SimpleRecognizerCorrect                                              
 0m06.64s | 460104 ko | Parsers/StringLike/Properties                                                
 0m06.59s | 515228 ko | Parsers/ContextFreeGrammar/Fix/Fix                                           
 0m05.73s | 454632 ko | Parsers/Grammars/Tests                                                       
 0m05.62s | 458036 ko | Common/Ensembles/IndexedEnsembles                                            
 0m05.41s | 586744 ko | Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflectiveOpt               
 0m05.41s | 586744 ko | ─change                                                                      
 0m05.17s | 521756 ko | Parsers/Refinement/FixedLengthLemmas                                         
 0m00.67s | 439784 ko | Parsers/ContextFreeGrammar/Carriers                                          
 0m00.67s | 432096 ko | Parsers/Reflective/Syntax                                                    
 0m00.66s | 436352 ko | Parsers/ContextFreeGrammar/Properties                                        
 0m00.66s | 437212 ko | Parsers/Reachable/ParenBalanced/Core                                         
 0m00.64s | 420168 ko | Common/LogicFacts                                                            
 0m00.64s | 430180 ko | Common/SumType                                                               
 0m00.64s | 441632 ko | Parsers/Reflective/Morphisms                                                 
 0m00.63s | 483176 ko | Parsers/ContextFreeGrammar/Fix/PreInterface                                  
 0m00.63s | 479928 ko | Parsers/SimpleRecognizerOptimized                                            
 0m00.63s | 445856 ko | Parsers/Splitters/BruteForce                                                 
 0m00.62s | 431208 ko | Common/i3list                                                                
 0m00.61s | 422888 ko | Parsers/ContextFreeGrammar/SimpleTransfer                                    
 0m00.59s | 455408 ko | Parsers/BooleanRecognizerCorrect                                             
 0m00.58s | 425780 ko | Common/NatFacts                                                              
 0m00.58s | 444152 ko | Parsers/GenericRecognizerEquality                                            
 0m00.58s | 495876 ko | Parsers/ParserImplementationOptimized                                        
 0m00.58s | 444120 ko | Parsers/Reachable/OnlyLast/ReachableParse                                    
 0m00.56s | 423508 ko | Common/String_as_OT                                                          
 0m00.56s | 481036 ko | Parsers/ContextFreeGrammar/Fix/Interface                                     
 0m00.55s | 441072 ko | ADTRefinement/GeneralBuildADTRefinements                                     
 0m00.54s | 436740 ko | ADTRefinement/GeneralRefinements                                             
 0m00.54s | 444424 ko | Parsers/Reachable/All/ReachableParse                                         
 0m00.54s | 438344 ko | Parsers/WellFoundedParseProperties                                           
 0m00.53s | 423316 ko | Common/SetEq                                                                 
 0m00.52s | 432912 ko | Common/ilist2                                                                
 0m00.52s | 456560 ko | Parsers/Reflective/ParserLogicalRelations                                    
 0m00.51s | 442928 ko | ADTRefinement/BuildADTRefinements/RefineAllMethods                           
 0m00.50s | 439244 ko | ADTRefinement/Refinements/ADTRepInv                                          
 0m00.49s | 506856 ko | Parsers/Refinement/ReductionTactics                                          
 0m00.48s | 434504 ko | Common/List/DisjointFacts                                                    
 0m00.48s | 441576 ko | Parsers/Reachable/MaybeEmpty/OfParse                                         
 0m00.47s | 446128 ko | Parsers/BooleanRecognizerEquality                                            
 0m00.47s | 443316 ko | Parsers/Reachable/OnlyFirst/ReachableParse                                   
 0m00.46s | 431484 ko | Parsers/ContextFreeGrammar/Reflective                                        
 0m00.46s | 455536 ko | Parsers/GenericRecognizerCorrect                                             
 0m00.45s | 437540 ko | Common/FixedPoints                                                           
 0m00.45s | 431632 ko | Common/Telescope/Equality                                                    
 0m00.45s | 429236 ko | Computation/Monad                                                            
 0m00.44s | 420204 ko | Common/BoolFacts                                                             
 0m00.44s | 420924 ko | Parsers/BaseTypesLemmas                                                      
 0m00.43s | 419788 ko | Common/Instances                                                             
 0m00.43s | 430136 ko | Computation/LogicLemmas                                                      
 0m00.42s | 434736 ko | Common/Enumerable/BoolProp                                                   
 0m00.42s | 421628 ko | Common/SetoidInstances                                                       
 0m00.42s | 454088 ko | Parsers/GenericRecognizerOptimizedTactics                                    
 0m00.42s | 469092 ko | Parsers/ParserInterfaceReflective                                            
 0m00.41s | 433088 ko | Common/List/Operations                                                       
 0m00.41s | 432596 ko | Computation/ApplyMonad                                                       
 0m00.41s | 447380 ko | Parsers/SimpleBooleanRecognizerEquality                                      
 0m00.40s | 432176 ko | Common/Gensym                                                                
 0m00.40s | 430236 ko | Common/List/FlattenList                                                      
 0m00.40s | 431484 ko | Common/ilist3

With the previous one:

     Time |  Peak Mem | File Name                                                                    
-----------------------------------------------------------------------------------------------------
10m51.99s | 890808 ko | Total Time / Peak Mem                                                        
-----------------------------------------------------------------------------------------------------
 0m37.99s | 694300 ko | Parsers/Refinement/PossibleTerminalsSets                                     
 0m36.96s | 661000 ko | Parsers/GenericRecognizerMin                                                 
 0m28.85s | 722848 ko | Parsers/ParserFromParserADT                                                  
 0m28.04s | 890808 ko | Parsers/BooleanRecognizerOptimized                                           
 0m22.41s | 818288 ko | Parsers/GenericRecognizerOptimized                                           
 0m20.56s | 845788 ko | Parsers/BooleanRecognizerOptimizedReflectiveCorrectness                      
 0m20.42s | 533896 ko | Common/FMapExtensions                                                        
 0m18.27s | 568320 ko | Parsers/SplitterFromParserADT                                                
 0m16.77s | 477272 ko | Parsers/Refinement/BinOpBrackets/MakeBinOpTable                              
 0m13.28s | 789144 ko | Parsers/Reflective/LogicalRelations                                          
 0m11.58s | 574960 ko | Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflective                  
 0m11.51s | 510584 ko | Common/List/ListFacts                                                        
 0m10.38s | 520696 ko | Parsers/ContextFreeGrammar/Fix/Fix                                           
 0m08.18s | 460208 ko | Parsers/StringLike/FirstCharSuchThat                                         
 0m08.11s | 496636 ko | Parsers/ContextFreeGrammar/Fix/ProdAbstractInterpretationDefinitions         
 0m07.42s | 457640 ko | Parsers/StringLike/Properties                                                
 0m07.41s | 503016 ko | Parsers/SimpleRecognizerCorrect                                              
 0m06.67s | 500760 ko | Parsers/ContextFreeGrammar/Fix/FixRelated                                    
 0m06.21s | 448928 ko | Parsers/AbstractInterpretation/NonTerminalMap                                
 0m06.18s | 457660 ko | Parsers/Grammars/Tests                                                       
 0m05.93s | 501564 ko | Parsers/MinimalParseOfParse                                                  
 0m05.88s | 517700 ko | Parsers/Refinement/FixedLengthLemmas                                         
 0m05.77s | 450668 ko | Common/Ensembles/IndexedEnsembles                                            
 0m05.69s | 586028 ko | Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflectiveOpt               
 0m05.69s | 586028 ko | ─change                                                                      
 0m05.62s | 498248 ko | Parsers/Grammars/JSONTests                                                   
 0m05.30s | 552752 ko | Parsers/Refinement/DisjointRulesRev                                          
 0m04.68s | 477508 ko | Common/FMapExtensions/LiftRelationInstances                                  
 0m04.57s | 499320 ko | Parsers/Refinement/EmptyLemmas                                               
 0m04.43s | 439640 ko | Parsers/Refinement/BinOpBrackets/ParenBalancedLemmas                         
 0m04.35s | 517564 ko | Parsers/BooleanRecognizerOptimizedReflective                                 
 0m04.20s | 440396 ko | Parsers/GenericRecognizerExt                                                 
 0m04.00s | 556080 ko | Parsers/Refinement/DisjointRules                                             
 0m03.77s | 465500 ko | Common/Wf2                                                                   
 0m03.77s | 441040 ko | Parsers/ContextFreeGrammar/Fix/Prod                                          
 0m03.77s | 465500 ko | ─rewrite                                                                     
 0m03.71s | 494436 ko | Parsers/ContextFreeGrammar/Fix/Correct                                       
 0m00.42s | 402980 ko | Parsers/BooleanRecognizerFull                                                
 0m00.42s | 418688 ko | Parsers/Reflective/ParserReify                                               
 0m00.42s | 413900 ko | Parsers/Reflective/ParserSemanticsOptimized                                  
 0m00.41s | 385384 ko | ADTNotation/BuildADTReplaceMethods                                           
 0m00.41s | 421428 ko | Common/Monad                                                                 
 0m00.41s | 420180 ko | Common/OptionFacts                                                           
 0m00.41s | 431672 ko | Common/Sigma                                                                 
 0m00.41s | 431448 ko | Common/i3list2                                                               
 0m00.41s | 430616 ko | Computation/LogicLemmas                                                      
 0m00.41s | 449536 ko | Parsers/BooleanRecognizerTests                                               
 0m00.41s | 418812 ko | Parsers/ContextFreeGrammar/TransferProperties                                
 0m00.41s | 435532 ko | Parsers/Grammars/JSON                                                        
 0m00.41s | 435740 ko | Parsers/Grammars/JSONImpoverished                                            
 0m00.40s | 380088 ko | ADTNotation/BuildADTSig                                                      
 0m00.40s | 411808 ko | Common/Ensembles/Cardinal                                                    
 0m00.40s | 419232 ko | Common/UIP                                                                   
 0m00.40s | 400908 ko | Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretationDefinitionsRelations
 0m00.40s | 396284 ko | Parsers/Grammars/ExpressionNumPlusParen                                      
 0m00.40s | 385148 ko | Parsers/Grammars/JSComment                                                   
 0m00.40s | 435212 ko | Parsers/Grammars/JSONImpoverishedOriginal                                    
 0m00.40s | 369708 ko | Parsers/Reflective/ParserSyntaxEquivalence                                   
 0m00.40s | 434268 ko | Parsers/Reflective/Semantics                                                 
 0m00.39s | 398788 ko | ADTNotation/BuildComputationalADT                                            
 0m00.39s | 405844 ko | ADTRefinement/BuildADTRefinements/AddCache                                   
 0m00.39s | 396804 ko | ADTRefinement/BuildADTSetoidMorphisms                                        
 0m00.39s | 427904 ko | ADTRefinement/Refinements/HoneRepresentation                                 
 0m00.39s | 422732 ko | Common/Enumerable/ReflectiveForall                                           
 0m00.39s | 367016 ko | Common/StringBound                                                           
 0m00.39s | 402168 ko | Common/i2list2                                                               
 0m00.39s | 389000 ko | Parsers/ContextFreeGrammar/Precompute                                        
 0m00.39s | 423316 ko | Parsers/ContextFreeGrammar/SimpleCorrectnessLemmas                           
 0m00.39s | 387936 ko | Parsers/Grammars/StringLiteral                                               
 0m00.39s | 390908 ko | Parsers/ParserInterface

Before the previous one:

    Time |  Peak Mem | File Name                                                                    
----------------------------------------------------------------------------------------------------
9m37.63s | 933836 ko | Total Time / Peak Mem                                                        
----------------------------------------------------------------------------------------------------
0m33.23s | 775788 ko | Parsers/GenericRecognizerMin                                                 
0m29.36s | 698040 ko | Parsers/Refinement/PossibleTerminalsSets                                     
0m25.21s | 723616 ko | Parsers/ParserFromParserADT                                                  
0m25.21s | 723616 ko | ─abstract                                                                    
0m23.13s | 933836 ko | Parsers/BooleanRecognizerOptimized                                           
0m19.05s | 847244 ko | Parsers/BooleanRecognizerOptimizedReflectiveCorrectness                      
0m18.63s | 823184 ko | Parsers/GenericRecognizerOptimized                                           
0m15.45s | 534308 ko | Common/FMapExtensions                                                        
0m15.35s | 573396 ko | Parsers/SplitterFromParserADT                                                
0m13.33s | 477880 ko | Parsers/Refinement/BinOpBrackets/MakeBinOpTable                              
0m11.52s | 652828 ko | Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflective                  
0m10.89s | 779920 ko | Parsers/Reflective/LogicalRelations                                          
0m08.76s | 511400 ko | Common/List/ListFacts                                                        
0m07.23s | 517236 ko | Parsers/ContextFreeGrammar/Fix/Fix                                           
0m06.48s | 458460 ko | Parsers/StringLike/FirstCharSuchThat                                         
0m06.11s | 552328 ko | Parsers/StringLike/LastChar                                                  
0m06.02s | 494920 ko | Parsers/ContextFreeGrammar/Fix/ProdAbstractInterpretationDefinitions         
0m06.01s | 456636 ko | Parsers/StringLike/Properties                                                
0m05.92s | 504320 ko | Parsers/MinimalParseOfParse                                                  
0m05.70s | 508800 ko | Parsers/SimpleRecognizerCorrect                                              
0m05.55s | 500388 ko | Parsers/ContextFreeGrammar/Fix/FixRelated                                    
0m05.32s | 456828 ko | Parsers/Grammars/Tests                                                       
0m04.95s | 519196 ko | Parsers/StringLike/OcamlString                                               
0m04.91s | 496504 ko | Parsers/Grammars/JSONTests                                                   
0m04.78s | 452300 ko | Common/Ensembles/IndexedEnsembles                                            
0m04.57s | 447912 ko | Parsers/AbstractInterpretation/NonTerminalMap                                
0m04.55s | 518928 ko | Parsers/Refinement/FixedLengthLemmas                                         
0m04.54s | 586256 ko | Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflectiveOpt               
0m04.54s | 586256 ko | ─change                                                                      
0m04.41s | 557204 ko | Parsers/Refinement/DisjointRulesRev                                          
0m04.08s | 475472 ko | Common/FMapExtensions/LiftRelationInstances                                  
0m03.78s | 517792 ko | Parsers/BooleanRecognizerOptimizedReflective                                 
0m03.77s | 569796 ko | Parsers/Refinement/DisjointRules                                             
0m03.77s | 492936 ko | Parsers/Refinement/EmptyLemmas                                               
0m03.61s | 437648 ko | Parsers/Refinement/BinOpBrackets/ParenBalancedLemmas                         
0m03.42s | 440732 ko | Parsers/GenericRecognizerExt                                                 
0m03.30s | 456264 ko | Parsers/Grammars/JavaScript                                                  
0m03.28s | 464584 ko | Common/Wf2                                                                   
0m03.11s | 578452 ko | Parsers/Refinement/SharpenedJSComment                                        
0m03.03s | 492544 ko | Parsers/ContextFreeGrammar/Fix/Correct                                       
0m02.92s | 442244 ko | Parsers/ContextFreeGrammar/Fix/Prod                                          
0m02.92s | 445884 ko | Parsers/Refinement/BinOpBrackets/ParenBalancedGrammar                        
0m02.79s | 490992 ko | Common/FMapExtensions/Wf                                                     
0m02.77s | 451540 ko | Parsers/Refinement/FinishingLemma                                            
0m02.71s | 445120 ko | Computation/Refinements/General                                              
0m02.69s | 435100 ko | Parsers/StringLike/ForallChars                                               
0m02.65s | 486076 ko | Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretation                    
0m02.54s | 444028 ko | Common/Ensembles/EnsembleListEquivalence                                     
0m02.51s | 627196 ko | Parsers/Refinement/SharpenedExpressionPlusParen                              
0m02.49s | 438592 ko | Parsers/Refinement/BinOpBrackets/ParenBalanced                               
0m02.48s | 624512 ko | Parsers/Refinement/SharpenedExpressionPlus                                   
0m02.47s | 574028 ko | Parsers/Refinement/BinOpBrackets/BinOpRules                                  
0m02.44s | 442052 ko | Common/List/ListMorphisms                                                    
0m02.42s | 448844 ko | Common                                                                       
0m02.37s | 453576 ko | Parsers/RecognizerPreOptimized                                               
0m02.36s | 451044 ko | Parsers/Reflective/SyntaxEquivalenceReflective                               
0m02.34s | 451188 ko | ADTRefinement/FixedPoint                                                     
0m02.33s | 437660 ko | Parsers/StringLike/LastCharSuchThat                                          
0m02.33s | 437660 ko | ─apply                                                                       
0m02.25s | 437948 ko | Parsers/Splitters/RDPList                                                    
0m02.16s | 568524 ko | Parsers/Refinement/SharpenedStringLiteral                                    
0m02.06s | 434440 ko | Common/Wf1                                                                   
0m02.06s | 434440 ko | ─rewrite                                                                     
0m02.00s | 430692 ko | Common/BoundedLookup                                                         
0m01.97s | 434648 ko | Common/Ensembles/CombinatorLaws                                              
0m01.93s | 615476 ko | Parsers/Refinement/SharpenedExpressionPlusParenParseTree                     
0m01.86s | 442868 ko | Parsers/GenericRecognizerBoolEquality                                        
0m01.86s | 436548 ko | Parsers/StringLike/FirstChar                                                 
0m01.84s | 561592 ko | Parsers/Refinement/SharpenedABStar                                           
0m01.75s | 370132 ko | Common/Frame                                                                 
0m01.69s | 440644 ko | Common/StringFacts                                                           
0m01.68s | 447268 ko | Parsers/Reachable/ParenBalancedHiding/MinimalOfCore                          
0m01.66s | 438684 ko | Common/Enumerable/ReflectiveForallAggregate                                  
0m01.62s | 453528 ko | Parsers/Reflective/SyntaxEquality                                            
0m01.58s | 436640 ko | Common/List/PermutationFacts                                                 
0m01.51s | 557328 ko | Parsers/Refinement/SharpenedExpressionParen                                  
0m01.50s | 554608 ko | Parsers/Refinement/DisjointLemmas                                            
0m01.47s | 429080 ko | Common/DecideableEnsembles                                                   
0m01.45s | 439816 ko | Common/SetEqProperties                                                       
0m01.45s | 436904 ko | Computation/FixComp                                                          
0m01.36s | 441084 ko | Parsers/Reachable/ParenBalanced/MinimalOfCore                                
0m01.35s | 441084 ko | ─destruct                                                                    
0m01.33s | 477512 ko | Parsers/ContextFreeGrammar/Fix/AsciiLattice                                  
0m01.32s | 441904 ko | Common/MSetExtensions                                                        
0m01.32s | 450904 ko | Computation/Refinements/Iterate_Decide_Comp                                  
0m01.32s | 433480 ko | Parsers/Grammars/JavaScriptAssignmentExpression                              
0m01.25s | 430728 ko | Computation/SetoidMorphisms                                                  
0m01.23s | 433660 ko | Parsers/StringLike/String                                                    
0m01.21s | 432264 ko | Computation/IfDec                                                            
0m01.19s | 434680 ko | Common/Ensembles/Morphisms                                                   
0m01.19s | 432164 ko | Common/Equality                                                              
0m01.16s | 447920 ko | Common/MSetBoundedLattice                                                    
0m01.15s | 465496 ko | Parsers/ParserImplementation                                                 
0m01.14s | 447276 ko | Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretationDefinitions         
0m01.13s | 438636 ko | Parsers/ContextFreeGrammar/Fix/Properties                                    
0m01.12s | 438408 ko | Common/IterateBoundedIndex                                                   
0m01.12s | 438408 ko | ─assert                                                                      
0m01.11s | 441188 ko | Computation/ListComputations                                                 
0m01.11s | 450892 ko | Parsers/Splitters/BruteForce                                                 
0m01.10s | 433156 ko | ADTRefinement/SetoidMorphisms                                                
0m01.08s | 442188 ko | Parsers/Reachable/ParenBalanced/OfParse                                      
0m01.06s | 439236 ko | ADTRefinement/BuildADTRefinements/HoneRepresentation                         
0m01.04s | 421608 ko | Common/NatFacts                                                              
0m01.02s | 439056 ko | Common/List/UpperBound                                                       
0m00.96s | 531036 ko | Parsers/ContextFreeGrammar/ExplorationUtil                                   
0m00.92s | 552316 ko | Parsers/Refinement/SharpenedABStarParseTree                                  
0m00.90s | 559828 ko | Parsers/Refinement/Tactics                                                   
0m00.87s | 435588 ko | Common/Enumerable                                                            
0m00.85s | 411520 ko | Computation/Decidable                                                        
0m00.85s | 494732 ko | Parsers/AbstractInterpretation/NonTerminalMapWf                              
0m00.83s | 430708 ko | Computation/FoldComp                                                         
0m00.80s | 436848 ko | Parsers/ContextFreeGrammar/ValidProperties                                   
0m00.79s | 432596 ko | Parsers/Reachable/OnlyLast/MinimalReachableOfReachable                       
0m00.79s | 549664 ko | Parsers/Refinement/ExtractSharpenedABStar                                    
0m00.78s | 430980 ko | Parsers/Reachable/MaybeEmpty/MinimalOfCore                                   
0m00.77s | 360252 ko | Common/Wf                                                                    
0m00.77s | 431064 ko | Parsers/Reachable/All/MinimalReachableOfReachable                            
0m00.76s | 551360 ko | Parsers/ExtrOcamlParsers                                                     
0m00.75s | 440960 ko | ADTRefinement/Refinements/ADTCache                                           
0m00.75s | 438784 ko | Parsers/ContextFreeGrammar/Fold                                              
0m00.74s | 432644 ko | Parsers/Reachable/OnlyFirst/MinimalReachableOfReachable                      
0m00.70s | 433808 ko | Parsers/ContextFreeGrammar/SimpleCorrectnessMorphisms                        
0m00.70s | 481684 ko | Parsers/SimpleRecognizerOptimized                                            
0m00.69s | 438060 ko | Parsers/ContextFreeGrammar/Fix/Definitions                                   
0m00.69s | 430848 ko | Parsers/Reflective/Syntax                                                    
0m00.67s | 438964 ko | Parsers/ContextFreeGrammar/Carriers                                          
0m00.66s | 430780 ko | Common/i3list                                                                
0m00.65s | 430348 ko | Common/SumType                                                               
0m00.64s | 440548 ko | ADTNotation/BuildADT                                                         
0m00.62s | 435612 ko | Parsers/ContextFreeGrammar/Properties                                        
0m00.62s | 497228 ko | Parsers/ParserImplementationOptimized                                        
0m00.62s | 442024 ko | Parsers/Reachable/OnlyLast/ReachableParse                                    
0m00.61s | 436672 ko | Parsers/Reachable/ParenBalanced/Core                                         
0m00.60s | 438380 ko | Parsers/ContextFreeGrammar/ValidReflective                                   
0m00.59s | 480656 ko | Parsers/ContextFreeGrammar/Fix/Interface                                     
0m00.59s | 480916 ko | Parsers/ContextFreeGrammar/Fix/PreInterface                                  
0m00.59s | 437820 ko | Parsers/WellFoundedParseProperties                                           
0m00.55s | 430432 ko | Common/ilist2                                                                
0m00.55s | 439728 ko | Parsers/Reachable/All/ReachableParse                                         
0m00.55s | 438824 ko | Parsers/Reflective/Morphisms                                                 
0m00.54s | 438384 ko | ADTRefinement/GeneralBuildADTRefinements                                     
0m00.54s | 438244 ko | ADTRefinement/Refinements/ADTRepInv                                          
0m00.54s | 457820 ko | Parsers/BooleanRecognizerCorrect                                             
0m00.54s | 444096 ko | Parsers/GenericRecognizerEquality                                            
0m00.54s | 454980 ko | Parsers/Reflective/ParserLogicalRelations                                    
0m00.53s | 435980 ko | ADTRefinement/GeneralRefinements                                             
0m00.51s | 440540 ko | ADTRefinement/BuildADTRefinements/RefineAllMethods                           
0m00.51s | 432744 ko | Common/List/DisjointFacts                                                    
0m00.51s | 408568 ko | Common/String_as_OT                                                          
0m00.51s | 440856 ko | Parsers/Reachable/MaybeEmpty/OfParse                                         
0m00.51s | 507544 ko | Parsers/Refinement/ReductionTactics                                          
0m00.50s | 470940 ko | Parsers/ParserInterfaceReflective                                            
0m00.49s | 434568 ko | Common/FixedPoints                                                           
0m00.49s | 387824 ko | Parsers/ContextFreeGrammar/SimpleTransfer                                    
0m00.49s | 457388 ko | Parsers/GenericRecognizerCorrect                                             
0m00.48s | 435120 ko | Common/Enumerable/BoolProp                                                   
0m00.48s | 442760 ko | Parsers/Reachable/OnlyFirst/ReachableParse                                   
0m00.47s | 431452 ko | Common/Gensym                                                                
0m00.47s | 351676 ko | Common/LogicFacts                                                            
0m00.47s | 437004 ko | Parsers/ContextFreeGrammar/Equality                                          
0m00.47s | 430344 ko | Parsers/ContextFreeGrammar/Reflective                                        
0m00.46s | 431836 ko | Common/ilist3                                                                
0m00.46s | 429164 ko | Computation/Monad                                                            
0m00.46s | 444840 ko | Parsers/BooleanRecognizerEquality                                            
0m00.45s | 432024 ko | Common/List/Operations                                                       
0m00.45s | 430848 ko | Common/Telescope/Equality                                                    
0m00.45s | 434648 ko | Parsers/Reflective/PartialUnfold                                             
0m00.45s | 437916 ko | Parsers/SimpleRecognizerExt                                                  
0m00.44s | 427868 ko | ADTRefinement/Refinements/HoneRepresentation                                 
0m00.44s | 429100 ko | Common/List/FlattenList                                                      
0m00.44s | 448560 ko | Parsers/BooleanRecognizerTests                                               
0m00.44s | 434116 ko | Parsers/Grammars/JSONImpoverished                                            
0m00.43s | 429772 ko | Common/ilist                                                                 
0m00.43s | 451760 ko | Parsers/GenericRecognizerOptimizedTactics                                    
0m00.43s | 434236 ko | Parsers/Grammars/JSONImpoverishedOriginal                                    
0m00.43s | 426108 ko | Parsers/Reflective/ParserSemantics                                           
0m00.43s | 413944 ko | Parsers/Reflective/ParserSemanticsOptimized                                  
0m00.43s | 426180 ko | Parsers/Reflective/ParserSoundness                                           
0m00.42s | 445168 ko | Parsers/ParserADTSpecification                                               
0m00.42s | 436168 ko | Parsers/Reflective/ParserSoundnessOptimized                                  
0m00.42s | 445372 ko | Parsers/SimpleBooleanRecognizerEquality                                      
0m00.41s | 432872 ko | Common/Sigma                                                                 
0m00.41s | 402212 ko | Common/i2list2                                                               
0m00.41s | 430000 ko | Computation/LogicLemmas                                                      
0m00.41s | 408508 ko | Parsers/BaseTypesLemmas                                                      
0m00.40s | 397384 ko | Common/Enumerable/ReflectiveForallStaged                                     
0m00.40s | 438640 ko | Parsers/BooleanRecognizerExt                                                 
0m00.40s | 402076 ko | Parsers/BooleanRecognizerFull                                                
0m00.40s | 399128 ko | Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretationDefinitionsRelations
0m00.40s | 372932 ko | Parsers/CorrectnessBaseTypes                                                 
0m00.40s | 386064 ko | Parsers/Grammars/StringLiteral                                               
0m00.40s | 368160 ko | Parsers/Reflective/ParserPartialUnfold                                       
0m00.40s | 433092 ko | Parsers/Reflective/Semantics                                                 
0m00.39s | 378008 ko | Common/Ensembles                                                             
0m00.39s | 390224 ko | Common/Ensembles/Equivalence                                                 
0m00.39s | 429788 ko | Computation/ApplyMonad                                                       
0m00.39s | 394100 ko | Parsers/Grammars/ExpressionNumPlusParen                                      
0m00.39s | 388824 ko | Parsers/Grammars/Trivial                                                     
0m00.39s | 383932 ko | Parsers/Reachable/ParenBalancedHiding/WellFounded                            
0m00.39s | 386696 ko | Parsers/Reflective/Reify                                                     
0m00.39s | 375640 ko | Parsers/Reflective/SemanticsOptimized                                        
0m00.39s | 411364 ko | Parsers/Reflective/SyntaxEquivalence                                         
0m00.38s | 372344 ko | ADT/ADTHide                                                                  
0m00.38s | 398236 ko | ADTInduction                                                                 
0m00.38s | 403580 ko | ADTRefinement/BuildADTRefinements/AddCache                                   
0m00.38s | 407596 ko | ADTRefinement/Refinements/RefineHideADT                                      
0m00.38s | 422428 ko | Common/Enumerable/ReflectiveForall                                           
0m00.38s | 429716 ko | Common/i3list2                                                               
0m00.38s | 389928 ko | Computation/FueledFix                                                        
0m00.38s | 371824 ko | Parsers/Grammars/ABStar                                                      
0m00.38s | 360808 ko | Parsers/Reachable/OnlyLast/ReachableWellFounded                              
0m00.38s | 368632 ko | Parsers/Reflective/Syntactify                                                
0m00.37s | 367068 ko | ADT                                                                          
0m00.37s | 384528 ko | ADTRefinement/BuildADTRefinements/SimplifyRep                                
0m00.37s | 387304 ko | Common/BoolFacts                                                             
0m00.37s | 413376 ko | Common/Ensembles/Cardinal                                                    
0m00.37s | 421732 ko | Common/Le                                                                    
0m00.37s | 391884 ko | Common/Prod                                                                  
0m00.37s | 378484 ko | Parsers/ContextFreeGrammar/Fix/Inject                                        
0m00.37s | 399224 ko | Parsers/ContextFreeGrammar/PreNotations                                      
0m00.37s | 368708 ko | Parsers/Grammars/EvalGrammarTactics                                          
0m00.37s | 369012 ko | Parsers/Reachable/OnlyLast/Reachable                                         
0m00.37s | 400472 ko | Parsers/Reachable/ParenBalancedHiding/Core                                   
0m00.37s | 419112 ko | Parsers/Refinement/PreTactics                                                
0m00.37s | 418900 ko | Parsers/Reflective/ParserReify                                               
0m00.36s | 371864 ko | ADT/ADTSig                                                                   
0m00.36s | 397988 ko | ADTNotation/BuildComputationalADT                                            
0m00.36s | 371384 ko | ADTRefinement/Refinements/SimplifyRep                                        
0m00.36s | 365752 ko | Common/StringBound                                                           
0m00.36s | 379356 ko | Parsers/ActionEvaluator                                                      
0m00.36s | 395496 ko | Parsers/ContextFreeGrammar/Notations                                         
0m00.36s | 386852 ko | Parsers/ContextFreeGrammar/PreNotationsLemmas                                
0m00.36s | 383860 ko | Parsers/Grammars/JSComment                                                   
0m00.36s | 432328 ko | Parsers/Grammars/JSON                                                        
0m00.36s | 379276 ko | Parsers/Reachable/ParenBalanced/WellFounded                                  
0m00.36s | 369864 ko | Parsers/Reflective/ParserSyntaxEquivalence                                   
0m00.35s | 384444 ko | ADTNotation/BuildADTReplaceMethods                                           
0m00.35s | 372600 ko | ADTRefinement                                                                
0m00.35s | 396912 ko | ADTRefinement/BuildADTSetoidMorphisms                                        
0m00.35s | 386288 ko | ADTRefinement/Core                                                           
0m00.35s | 401288 ko | ADTRefinement/GeneralBuildADTTactics                                         
0m00.35s | 379896 ko | ADTRefinement/Refinements/DelegateMethods                                    
0m00.35s | 421252 ko | Common/Telescope/Instances                                                   
0m00.35s | 393836 ko | Common/ilist3_pair                                                           
0m00.35s | 361744 ko | Computation                                                                  
0m00.35s | 356512 ko | Computation/Refinements/Tactics                                              
0m00.35s | 363200 ko | Computation/SetoidEqMorphisms                                                
0m00.35s | 377984 ko | Parsers/ContextFreeGrammar/ReflectiveLemmas                                  
0m00.35s | 416548 ko | Parsers/ContextFreeGrammar/TransferProperties                                
0m00.35s | 374736 ko | Parsers/Grammars/FlatComments                                                
0m00.35s | 394008 ko | Parsers/ParserInterface                                                      
0m00.34s | 379228 ko | ADTNotation/BuildADTSig                                                      
0m00.34s | 369976 ko | ADTRefinement/Refinements                                                    
0m00.34s | 347636 ko | Common/SetEq                                                                 
0m00.34s | 428900 ko | Computation/Core                                                             
0m00.34s | 385864 ko | Parsers/ContextFreeGrammar/Precompute                                        
0m00.34s | 367380 ko | Parsers/Reachable/All/Reachable                                              
0m00.34s | 365720 ko | Parsers/Reachable/MaybeEmpty/Core                                            
0m00.34s | 362896 ko | Parsers/Reflective/ParserSyntax                                              
0m00.34s | 355272 ko | Parsers/Specification                                                        
0m00.34s | 372892 ko | Parsers/StringLike                                                           
0m00.33s | 381940 ko | ADT/ComputationalADT                                                         
0m00.33s | 370656 ko | ADTNotation                                                                  
0m00.33s | 367844 ko | Parsers/GenericRecognizer                                                    
0m00.33s | 370120 ko | Parsers/Grammars/ExpressionParen                                             
0m00.33s | 367844 ko | ─generalize

mattam82 commented 3 years ago

I'd rather move on to more interesting things than rework the whole dev to come back to the timings of before (and probably we can go even much faster with the proper declarations everywhere). Are you guys fine with this small bump in overall compile time? (I'll run a bench on the Coq side to confirm the numbers)

JasonGross commented 3 years ago

I'm running a bench on my machine and will post the diffs between various commits here once it's done.

In any case, though, the parsers part of this project is maintained just enough to provide testing results for Coq's CI, and I'm fine with accepting small slowdowns when developer time is better spent elsewhere, and the slowdowns are not indicative of the underlying tactics becoming slower, but are rather artifacts of the instances we set up.

JasonGross commented 3 years ago

Diff between 395460462593193233975c071133dd9cab876939 (after) and c1fa14cecd51d31dfbcb7a928e6b470ac27b42e4 (before)

``` 3954604 | Peak Mem | File Name | c1fa14c | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ 7m33.62s | 871524 ko | Total Time / Peak Mem | 7m32.72s | 871476 ko || +0m00.89s || 48 ko | +0.19% | +0.00% ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ 0m22.99s | 739404 ko | Parsers/ParserFromParserADT | 0m22.95s | 739372 ko || +0m00.03s || 32 ko | +0.17% | +0.00% 0m21.83s | 694420 ko | Parsers/GenericRecognizerMin | 0m22.00s | 694592 ko || -0m00.17s || -172 ko | -0.77% | -0.02% 0m20.94s | 597468 ko | Parsers/Refinement/PossibleTerminalsSets | 0m20.76s | 594672 ko || +0m00.17s || 2796 ko | +0.86% | +0.47% 0m19.77s | 871524 ko | Parsers/BooleanRecognizerOptimized | 0m19.77s | 871476 ko || +0m00.00s || 48 ko | +0.00% | +0.00% 0m16.09s | 816256 ko | Parsers/BooleanRecognizerOptimizedReflectiveCorrectness | 0m16.45s | 816172 ko || -0m00.35s || 84 ko | -2.18% | +0.01% 0m15.83s | 795452 ko | Parsers/GenericRecognizerOptimized | 0m15.48s | 800004 ko || +0m00.34s || -4552 ko | +2.26% | -0.56% 0m14.15s | 571080 ko | Parsers/SplitterFromParserADT | 0m14.26s | 571096 ko || -0m00.10s || -16 ko | -0.77% | -0.00% 0m10.93s | 480164 ko | Common/FMapExtensions | 0m10.79s | 479956 ko || +0m00.14s || 208 ko | +1.29% | +0.04% 0m10.88s | 466700 ko | Parsers/Refinement/BinOpBrackets/MakeBinOpTable | 0m10.76s | 466616 ko || +0m00.12s || 84 ko | +1.11% | +0.01% 0m10.28s | 796332 ko | Parsers/Reflective/LogicalRelations | 0m10.23s | 796392 ko || +0m00.04s || -60 ko | +0.48% | -0.00% 0m09.41s | 635928 ko | Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflective | 0m09.37s | 636264 ko || +0m00.04s || -336 ko | +0.42% | -0.05% 0m07.46s | 511744 ko | Parsers/ContextFreeGrammar/Fix/Fix | 0m06.73s | 511700 ko || +0m00.72s || 44 ko | +10.84% | +0.00% 0m06.15s | 470016 ko | Common/List/ListFacts | 0m06.04s | 470052 ko || +0m00.11s || -36 ko | +1.82% | -0.00% 0m05.30s | 551376 ko | Parsers/StringLike/LastChar | 0m05.52s | 546700 ko || -0m00.21s || 4676 ko | -3.98% | +0.85% 0m04.89s | 499400 ko | Parsers/ContextFreeGrammar/Fix/FixRelated | 0m04.69s | 499396 ko || +0m00.19s || 4 ko | +4.26% | +0.00% 0m04.82s | 506916 ko | Parsers/MinimalParseOfParse | 0m04.57s | 506976 ko || +0m00.25s || -60 ko | +5.47% | -0.01% 0m04.69s | 445176 ko | Parsers/StringLike/Properties | 0m04.78s | 445172 ko || -0m00.08s || 4 ko | -1.88% | +0.00% 0m04.57s | 569860 ko | Parsers/Refinement/DisjointRulesRev | 0m04.54s | 569780 ko || +0m00.03s || 80 ko | +0.66% | +0.01% 0m04.56s | 441504 ko | Parsers/StringLike/FirstCharSuchThat | 0m04.59s | 441544 ko || -0m00.03s || -40 ko | -0.65% | -0.00% 0m04.32s | 509220 ko | Parsers/StringLike/OcamlString | 0m04.28s | 509336 ko || +0m00.04s || -116 ko | +0.93% | -0.02% 0m04.31s | 488716 ko | Parsers/Grammars/JSONTests | 0m04.35s | 488712 ko || -0m00.04s || 4 ko | -0.91% | +0.00% 0m04.29s | 452720 ko | Parsers/Grammars/Tests | 0m04.49s | 452788 ko || -0m00.20s || -68 ko | -4.45% | -0.01% 0m04.04s | 451448 ko | Parsers/AbstractInterpretation/NonTerminalMap | 0m03.97s | 451236 ko || +0m00.06s || 212 ko | +1.76% | +0.04% 0m03.79s | 558180 ko | Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflectiveOpt | 0m03.74s | 558300 ko || +0m00.04s || -120 ko | +1.33% | -0.02% 0m03.70s | 580392 ko | Parsers/Refinement/DisjointRules | 0m03.68s | 580308 ko || +0m00.02s || 84 ko | +0.54% | +0.01% 0m03.59s | 460212 ko | Parsers/ContextFreeGrammar/Fix/ProdAbstractInterpretationDefinitions | 0m03.63s | 460120 ko || -0m00.04s || 92 ko | -1.10% | +0.01% 0m03.52s | 440696 ko | Common/Ensembles/IndexedEnsembles | 0m03.50s | 440680 ko || +0m00.02s || 16 ko | +0.57% | +0.00% 0m03.46s | 477040 ko | Common/FMapExtensions/LiftRelationInstances | 0m03.44s | 476948 ko || +0m00.02s || 92 ko | +0.58% | +0.01% 0m03.31s | 506076 ko | Parsers/BooleanRecognizerOptimizedReflective | 0m03.21s | 506064 ko || +0m00.10s || 12 ko | +3.11% | +0.00% 0m03.21s | 454104 ko | Parsers/Grammars/JavaScript | 0m03.21s | 454036 ko || +0m00.00s || 68 ko | +0.00% | +0.01% 0m03.03s | 440836 ko | Parsers/Refinement/BinOpBrackets/ParenBalancedLemmas | 0m03.01s | 440936 ko || +0m00.02s || -100 ko | +0.66% | -0.02% 0m02.87s | 467900 ko | Parsers/SimpleRecognizerCorrect | 0m02.95s | 467288 ko || -0m00.08s || 612 ko | -2.71% | +0.13% 0m02.86s | 445820 ko | Parsers/GenericRecognizerExt | 0m02.80s | 445788 ko || +0m00.06s || 32 ko | +2.14% | +0.00% 0m02.84s | 592332 ko | Parsers/Refinement/SharpenedJSComment | 0m02.84s | 592420 ko || +0m00.00s || -88 ko | +0.00% | -0.01% 0m02.80s | 462384 ko | Common/Wf2 | 0m02.82s | 462284 ko || -0m00.02s || 100 ko | -0.70% | +0.02% 0m02.73s | 452860 ko | Parsers/Refinement/FinishingLemma | 0m02.77s | 452932 ko || -0m00.04s || -72 ko | -1.44% | -0.01% 0m02.72s | 496736 ko | Parsers/Refinement/EmptyLemmas | 0m02.58s | 496732 ko || +0m00.14s || 4 ko | +5.42% | +0.00% 0m02.63s | 499716 ko | Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretation | 0m02.66s | 497196 ko || -0m00.03s || 2520 ko | -1.12% | +0.50% 0m02.62s | 492152 ko | Common/FMapExtensions/Wf | 0m02.59s | 492292 ko || +0m00.03s || -140 ko | +1.15% | -0.02% 0m02.51s | 631124 ko | Parsers/Refinement/SharpenedExpressionPlus | 0m02.50s | 631176 ko || +0m00.00s || -52 ko | +0.39% | -0.00% 0m02.49s | 445048 ko | Parsers/Refinement/BinOpBrackets/ParenBalancedGrammar | 0m02.43s | 445164 ko || +0m00.06s || -116 ko | +2.46% | -0.02% 0m02.49s | 496196 ko | Parsers/Refinement/FixedLengthLemmas | 0m02.54s | 496412 ko || -0m00.04s || -216 ko | -1.96% | -0.04% 0m02.38s | 585060 ko | Parsers/Refinement/BinOpBrackets/BinOpRules | 0m02.42s | 585004 ko || -0m00.04s || 56 ko | -1.65% | +0.00% 0m02.36s | 438480 ko | Parsers/StringLike/ForallChars | 0m02.37s | 438360 ko || -0m00.01s || 120 ko | -0.42% | +0.02% 0m02.34s | 634832 ko | Parsers/Refinement/SharpenedExpressionPlusParen | 0m02.36s | 634792 ko || -0m00.02s || 40 ko | -0.84% | +0.00% 0m02.30s | 444728 ko | Parsers/ContextFreeGrammar/Fix/Prod | 0m02.34s | 444724 ko || -0m00.04s || 4 ko | -1.70% | +0.00% 0m02.04s | 444784 ko | Parsers/Refinement/BinOpBrackets/ParenBalanced | 0m01.98s | 444644 ko || +0m00.06s || 140 ko | +3.03% | +0.03% 0m02.04s | 439196 ko | Parsers/Splitters/RDPList | 0m02.06s | 439140 ko || -0m00.02s || 56 ko | -0.97% | +0.01% 0m01.98s | 496800 ko | Parsers/ContextFreeGrammar/Fix/Correct | 0m02.09s | 496372 ko || -0m00.10s || 428 ko | -5.26% | +0.08% 0m01.95s | 581664 ko | Parsers/Refinement/SharpenedStringLiteral | 0m01.93s | 581660 ko || +0m00.02s || 4 ko | +1.03% | +0.00% 0m01.93s | 437908 ko | Common/List/ListMorphisms | 0m01.83s | 437956 ko || +0m00.09s || -48 ko | +5.46% | -0.01% 0m01.92s | 452560 ko | ADTRefinement/FixedPoint | 0m02.02s | 452480 ko || -0m00.10s || 80 ko | -4.95% | +0.01% 0m01.89s | 443036 ko | Computation/Refinements/General | 0m01.88s | 443020 ko || +0m00.01s || 16 ko | +0.53% | +0.00% 0m01.80s | 431784 ko | Common/BoundedLookup | 0m01.79s | 431720 ko || +0m00.01s || 64 ko | +0.55% | +0.01% 0m01.80s | 440848 ko | Parsers/StringLike/LastCharSuchThat | 0m01.79s | 440788 ko || +0m00.01s || 60 ko | +0.55% | +0.01% 0m01.71s | 432404 ko | Common/Frame | 0m01.66s | 432684 ko || +0m00.05s || -280 ko | +3.01% | -0.06% 0m01.66s | 441792 ko | Common/Wf1 | 0m01.73s | 441688 ko || -0m00.07s || 104 ko | -4.04% | +0.02% 0m01.64s | 451092 ko | Parsers/RecognizerPreOptimized | 0m01.68s | 450972 ko || -0m00.04s || 120 ko | -2.38% | +0.02% 0m01.63s | 437024 ko | Common/Ensembles/EnsembleListEquivalence | 0m01.66s | 436992 ko || -0m00.03s || 32 ko | -1.80% | +0.00% 0m01.61s | 627688 ko | Parsers/Refinement/SharpenedExpressionPlusParenParseTree | 0m01.64s | 627676 ko || -0m00.02s || 12 ko | -1.82% | +0.00% 0m01.59s | 443372 ko | Common/StringFacts | 0m01.58s | 443288 ko || +0m00.01s || 84 ko | +0.63% | +0.01% 0m01.58s | 448436 ko | Parsers/GenericRecognizerBoolEquality | 0m01.60s | 448408 ko || -0m00.02s || 28 ko | -1.25% | +0.00% 0m01.55s | 573596 ko | Parsers/Refinement/SharpenedABStar | 0m01.51s | 573536 ko || +0m00.04s || 60 ko | +2.64% | +0.01% 0m01.50s | 437976 ko | Common | 0m01.53s | 438084 ko || -0m00.03s || -108 ko | -1.96% | -0.02% 0m01.43s | 455860 ko | Parsers/Reachable/ParenBalancedHiding/MinimalOfCore | 0m01.43s | 455968 ko || +0m00.00s || -108 ko | +0.00% | -0.02% 0m01.42s | 570880 ko | Parsers/Refinement/SharpenedExpressionParen | 0m01.35s | 570752 ko || +0m00.06s || 128 ko | +5.18% | +0.02% 0m01.42s | 441680 ko | Parsers/StringLike/FirstChar | 0m01.39s | 441656 ko || +0m00.03s || 24 ko | +2.15% | +0.00% 0m01.40s | 464040 ko | Parsers/Reflective/SyntaxEquality | 0m01.43s | 464024 ko || -0m00.03s || 16 ko | -2.09% | +0.00% 0m01.33s | 438640 ko | Parsers/Reflective/SyntaxEquivalenceReflective | 0m01.34s | 438696 ko || -0m00.01s || -56 ko | -0.74% | -0.01% 0m01.28s | 448472 ko | Parsers/Grammars/JavaScriptAssignmentExpression | 0m01.28s | 448388 ko || +0m00.00s || 84 ko | +0.00% | +0.01% 0m01.23s | 442480 ko | Common/List/PermutationFacts | 0m01.28s | 442516 ko || -0m00.05s || -36 ko | -3.90% | -0.00% 0m01.23s | 451880 ko | Parsers/Reachable/ParenBalanced/MinimalOfCore | 0m01.20s | 451972 ko || +0m00.03s || -92 ko | +2.50% | -0.02% 0m01.18s | 430212 ko | Common/DecideableEnsembles | 0m01.15s | 430156 ko || +0m00.03s || 56 ko | +2.60% | +0.01% 0m01.17s | 443036 ko | Computation/FixComp | 0m01.19s | 443088 ko || -0m00.02s || -52 ko | -1.68% | -0.01% 0m01.09s | 564632 ko | Parsers/Refinement/DisjointLemmas | 0m01.14s | 564628 ko || -0m00.04s || 4 ko | -4.38% | +0.00% 0m01.09s | 457168 ko | Parsers/Splitters/BruteForce | 0m01.09s | 456540 ko || +0m00.00s || 628 ko | +0.00% | +0.13% 0m01.07s | 486712 ko | Parsers/ContextFreeGrammar/Fix/AsciiLattice | 0m01.07s | 486540 ko || +0m00.00s || 172 ko | +0.00% | +0.03% 0m01.06s | 436528 ko | Common/Enumerable/ReflectiveForallAggregate | 0m01.07s | 436604 ko || -0m00.01s || -76 ko | -0.93% | -0.01% 0m01.06s | 469416 ko | Parsers/ParserImplementation | 0m01.09s | 469312 ko || -0m00.03s || 104 ko | -2.75% | +0.02% 0m01.04s | 437756 ko | Common/NatFacts | 0m00.99s | 437656 ko || +0m00.05s || 100 ko | +5.05% | +0.02% 0m01.04s | 454608 ko | Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretationDefinitions | 0m01.03s | 454712 ko || +0m00.01s || -104 ko | +0.97% | -0.02% 0m01.03s | 451468 ko | Common/MSetBoundedLattice | 0m00.97s | 452344 ko || +0m00.06s || -876 ko | +6.18% | -0.19% 0m01.02s | 436388 ko | Common/SetEqProperties | 0m01.03s | 436440 ko || -0m00.01s || -52 ko | -0.97% | -0.01% 0m01.00s | 443132 ko | Common/MSetExtensions | 0m01.01s | 443028 ko || -0m00.01s || 104 ko | -0.99% | +0.02% 0m00.99s | 448696 ko | Computation/Refinements/Iterate_Decide_Comp | 0m01.01s | 448652 ko || -0m00.02s || 44 ko | -1.98% | +0.00% 0m00.98s | 437876 ko | Parsers/StringLike/String | 0m00.96s | 437816 ko || +0m00.02s || 60 ko | +2.08% | +0.01% 0m00.97s | 433048 ko | Common/Equality | 0m00.94s | 433156 ko || +0m00.03s || -108 ko | +3.19% | -0.02% 0m00.95s | 431352 ko | Common/Ensembles/CombinatorLaws | 0m00.95s | 431388 ko || +0m00.00s || -36 ko | +0.00% | -0.00% 0m00.93s | 431656 ko | Computation/SetoidMorphisms | 0m00.92s | 431716 ko || +0m00.01s || -60 ko | +1.08% | -0.01% 0m00.91s | 450760 ko | Parsers/Reachable/ParenBalanced/OfParse | 0m00.92s | 450928 ko || -0m00.01s || -168 ko | -1.08% | -0.03% 0m00.90s | 435196 ko | Computation/IfDec | 0m00.89s | 435220 ko || +0m00.01s || -24 ko | +1.12% | -0.00% 0m00.90s | 444176 ko | Parsers/ContextFreeGrammar/Fix/Properties | 0m00.96s | 444292 ko || -0m00.05s || -116 ko | -6.24% | -0.02% 0m00.89s | 540460 ko | Parsers/ContextFreeGrammar/ExplorationUtil | 0m00.87s | 540324 ko || +0m00.02s || 136 ko | +2.29% | +0.02% 0m00.86s | 508196 ko | Parsers/AbstractInterpretation/NonTerminalMapWf | 0m00.88s | 507988 ko || -0m00.02s || 208 ko | -2.27% | +0.04% 0m00.84s | 436116 ko | ADTRefinement/SetoidMorphisms | 0m00.85s | 436052 ko || -0m00.01s || 64 ko | -1.17% | +0.01% 0m00.83s | 572280 ko | Parsers/Refinement/Tactics | 0m00.83s | 572332 ko || +0m00.00s || -52 ko | +0.00% | -0.00% 0m00.80s | 442156 ko | ADTRefinement/BuildADTRefinements/HoneRepresentation | 0m00.80s | 442340 ko || +0m00.00s || -184 ko | +0.00% | -0.04% 0m00.79s | 567004 ko | Parsers/Refinement/SharpenedABStarParseTree | 0m00.80s | 566884 ko || -0m00.01s || 120 ko | -1.25% | +0.02% 0m00.78s | 438468 ko | Common/Enumerable | 0m00.79s | 438500 ko || -0m00.01s || -32 ko | -1.26% | -0.00% 0m00.76s | 428888 ko | Computation/Decidable | 0m00.76s | 428784 ko || +0m00.00s || 104 ko | +0.00% | +0.02% 0m00.73s | 443572 ko | Computation/ListComputations | 0m00.70s | 443552 ko || +0m00.03s || 20 ko | +4.28% | +0.00% 0m00.71s | 435172 ko | Common/IterateBoundedIndex | 0m00.73s | 435076 ko || -0m00.02s || 96 ko | -2.73% | +0.02% 0m00.71s | 444224 ko | Parsers/ContextFreeGrammar/ValidProperties | 0m00.69s | 444304 ko || +0m00.02s || -80 ko | +2.89% | -0.01% 0m00.71s | 566276 ko | Parsers/ExtrOcamlParsers | 0m00.68s | 566252 ko || +0m00.02s || 24 ko | +4.41% | +0.00% 0m00.68s | 429096 ko | Common/Wf | 0m00.73s | 429120 ko || -0m00.04s || -24 ko | -6.84% | -0.00% 0m00.68s | 438668 ko | Parsers/Reachable/OnlyLast/MinimalReachableOfReachable | 0m00.68s | 438784 ko || +0m00.00s || -116 ko | +0.00% | -0.02% 0m00.67s | 437296 ko | Common/List/UpperBound | 0m00.67s | 437208 ko || +0m00.00s || 88 ko | +0.00% | +0.02% 0m00.67s | 437640 ko | Parsers/Reachable/MaybeEmpty/MinimalOfCore | 0m00.67s | 437764 ko || +0m00.00s || -124 ko | +0.00% | -0.02% 0m00.66s | 440424 ko | Parsers/ContextFreeGrammar/Fix/Definitions | 0m00.65s | 440364 ko || +0m00.01s || 60 ko | +1.53% | +0.01% 0m00.65s | 431324 ko | Common/Ensembles/Morphisms | 0m00.65s | 431284 ko || +0m00.00s || 40 ko | +0.00% | +0.00% 0m00.65s | 432508 ko | Computation/FoldComp | 0m00.63s | 432664 ko || +0m00.02s || -156 ko | +3.17% | -0.03% 0m00.65s | 437492 ko | Parsers/Reachable/All/MinimalReachableOfReachable | 0m00.70s | 437424 ko || -0m00.04s || 68 ko | -7.14% | +0.01% 0m00.65s | 438672 ko | Parsers/Reachable/OnlyFirst/MinimalReachableOfReachable | 0m00.67s | 438496 ko || -0m00.02s || 176 ko | -2.98% | +0.04% 0m00.65s | 564160 ko | Parsers/Refinement/ExtractSharpenedABStar | 0m00.75s | 564244 ko || -0m00.09s || -84 ko | -13.33% | -0.01% 0m00.65s | 483588 ko | Parsers/SimpleRecognizerOptimized | 0m00.63s | 483500 ko || +0m00.02s || 88 ko | +3.17% | +0.01% 0m00.63s | 444048 ko | Parsers/ContextFreeGrammar/Fold | 0m00.56s | 444004 ko || +0m00.06s || 44 ko | +12.49% | +0.00% 0m00.62s | 441160 ko | ADTRefinement/Refinements/ADTCache | 0m00.59s | 441164 ko || +0m00.03s || -4 ko | +5.08% | -0.00% 0m00.62s | 438380 ko | Parsers/ContextFreeGrammar/Properties | 0m00.57s | 438644 ko || +0m00.05s || -264 ko | +8.77% | -0.06% 0m00.61s | 439996 ko | ADTNotation/BuildADT | 0m00.58s | 440136 ko || +0m00.03s || -140 ko | +5.17% | -0.03% 0m00.61s | 442804 ko | Parsers/ContextFreeGrammar/ValidReflective | 0m00.60s | 442848 ko || +0m00.01s || -44 ko | +1.66% | -0.00% 0m00.59s | 434172 ko | Common/SumType | 0m00.61s | 434228 ko || -0m00.02s || -56 ko | -3.27% | -0.01% 0m00.59s | 444368 ko | Parsers/Reachable/OnlyLast/ReachableParse | 0m00.58s | 444612 ko || +0m00.01s || -244 ko | +1.72% | -0.05% 0m00.57s | 419800 ko | Parsers/ContextFreeGrammar/Fix/PreInterface | 0m00.60s | 419732 ko || -0m00.03s || 68 ko | -5.00% | +0.01% 0m00.57s | 441924 ko | Parsers/Reflective/Syntax | 0m00.60s | 442024 ko || -0m00.03s || -100 ko | -5.00% | -0.02% 0m00.56s | 431656 ko | Common/i3list | 0m00.53s | 431696 ko || +0m00.03s || -40 ko | +5.66% | -0.00% 0m00.56s | 437684 ko | Parsers/Reachable/ParenBalanced/Core | 0m00.55s | 437656 ko || +0m00.01s || 28 ko | +1.81% | +0.00% 0m00.55s | 438864 ko | ADTRefinement/GeneralRefinements | 0m00.54s | 438832 ko || +0m00.01s || 32 ko | +1.85% | +0.00% 0m00.55s | 448904 ko | Parsers/GenericRecognizerEquality | 0m00.54s | 448988 ko || +0m00.01s || -84 ko | +1.85% | -0.01% 0m00.55s | 496088 ko | Parsers/ParserImplementationOptimized | 0m00.53s | 496144 ko || +0m00.02s || -56 ko | +3.77% | -0.01% 0m00.54s | 438884 ko | Parsers/ContextFreeGrammar/Carriers | 0m00.57s | 438972 ko || -0m00.02s || -88 ko | -5.26% | -0.02% 0m00.54s | 458008 ko | Parsers/Reflective/ParserLogicalRelations | 0m00.53s | 457964 ko || +0m00.01s || 44 ko | +1.88% | +0.00% 0m00.53s | 492472 ko | Parsers/ContextFreeGrammar/Fix/Interface | 0m00.52s | 492536 ko || +0m00.01s || -64 ko | +1.92% | -0.01% 0m00.53s | 436168 ko | Parsers/ContextFreeGrammar/SimpleCorrectnessMorphisms | 0m00.57s | 436248 ko || -0m00.03s || -80 ko | -7.01% | -0.01% 0m00.52s | 422260 ko | Common/String_as_OT | 0m00.50s | 422348 ko || +0m00.02s || -88 ko | +4.00% | -0.02% 0m00.51s | 443640 ko | Parsers/Reflective/Morphisms | 0m00.50s | 443700 ko || +0m00.01s || -60 ko | +2.00% | -0.01% 0m00.50s | 443272 ko | Parsers/WellFoundedParseProperties | 0m00.54s | 443352 ko || -0m00.04s || -80 ko | -7.40% | -0.01% 0m00.49s | 432568 ko | Common/ilist2 | 0m00.50s | 432540 ko || -0m00.01s || 28 ko | -2.00% | +0.00% 0m00.49s | 441876 ko | Parsers/Reachable/MaybeEmpty/OfParse | 0m00.46s | 441920 ko || +0m00.02s || -44 ko | +6.52% | -0.00% 0m00.48s | 460240 ko | Parsers/BooleanRecognizerCorrect | 0m00.50s | 460208 ko || -0m00.02s || 32 ko | -4.00% | +0.00% 0m00.47s | 442700 ko | ADTRefinement/BuildADTRefinements/RefineAllMethods | 0m00.46s | 442580 ko || +0m00.00s || 120 ko | +2.17% | +0.02% 0m00.47s | 445408 ko | Parsers/Reachable/All/ReachableParse | 0m00.47s | 445392 ko || +0m00.00s || 16 ko | +0.00% | +0.00% 0m00.46s | 441452 ko | ADTRefinement/GeneralBuildADTRefinements | 0m00.51s | 441568 ko || -0m00.04s || -116 ko | -9.80% | -0.02% 0m00.46s | 435576 ko | Common/FixedPoints | 0m00.47s | 435484 ko || -0m00.00s || 92 ko | -2.12% | +0.02% 0m00.46s | 420388 ko | Common/LogicFacts | 0m00.43s | 420532 ko || +0m00.03s || -144 ko | +6.97% | -0.03% 0m00.46s | 446168 ko | Parsers/BooleanRecognizerEquality | 0m00.49s | 446140 ko || -0m00.02s || 28 ko | -6.12% | +0.00% 0m00.46s | 428348 ko | Parsers/GenericRecognizerOptimizedTactics | 0m00.42s | 428324 ko || +0m00.04s || 24 ko | +9.52% | +0.00% 0m00.46s | 416508 ko | Parsers/Reachable/OnlyFirst/ReachableParse | 0m00.43s | 416500 ko || +0m00.03s || 8 ko | +6.97% | +0.00% 0m00.45s | 438848 ko | ADTRefinement/Refinements/ADTRepInv | 0m00.45s | 438904 ko || +0m00.00s || -56 ko | +0.00% | -0.01% 0m00.45s | 435632 ko | Common/List/DisjointFacts | 0m00.43s | 435528 ko || +0m00.02s || 104 ko | +4.65% | +0.02% 0m00.45s | 506332 ko | Parsers/Refinement/ReductionTactics | 0m00.44s | 506088 ko || +0m00.01s || 244 ko | +2.27% | +0.04% 0m00.45s | 381908 ko | Parsers/SimpleBooleanRecognizerEquality | 0m00.43s | 381936 ko || +0m00.02s || -28 ko | +4.65% | -0.00% 0m00.44s | 400304 ko | Parsers/GenericRecognizerCorrect | 0m00.46s | 400396 ko || -0m00.02s || -92 ko | -4.34% | -0.02% 0m00.44s | 445616 ko | Parsers/ParserInterfaceReflective | 0m00.39s | 445580 ko || +0m00.04s || 36 ko | +12.82% | +0.00% 0m00.43s | 432320 ko | Common/Gensym | 0m00.41s | 432436 ko || +0m00.02s || -116 ko | +4.87% | -0.02% 0m00.43s | 360636 ko | Computation/Monad | 0m00.41s | 360708 ko || +0m00.02s || -72 ko | +4.87% | -0.01% 0m00.42s | 433444 ko | Common/Sigma | 0m00.38s | 433324 ko || +0m00.03s || 120 ko | +10.52% | +0.02% 0m00.42s | 422124 ko | Parsers/BaseTypesLemmas | 0m00.37s | 422120 ko || +0m00.04s || 4 ko | +13.51% | +0.00% 0m00.42s | 368128 ko | Parsers/ContextFreeGrammar/Reflective | 0m00.40s | 368128 ko || +0m00.01s || 0 ko | +4.99% | +0.00% 0m00.42s | 365056 ko | Parsers/SimpleRecognizerExt | 0m00.42s | 364932 ko || +0m00.00s || 124 ko | +0.00% | +0.03% 0m00.41s | 433520 ko | Common/List/Operations | 0m00.40s | 433320 ko || +0m00.00s || 200 ko | +2.49% | +0.04% 0m00.41s | 432548 ko | Common/ilist3 | 0m00.45s | 432548 ko || -0m00.04s || 0 ko | -8.88% | +0.00% 0m00.41s | 393116 ko | Parsers/Reflective/ParserReify | 0m00.40s | 393020 ko || +0m00.00s || 96 ko | +2.49% | +0.02% 0m00.40s | 341868 ko | Common/Enumerable/BoolProp | 0m00.39s | 341696 ko || +0m00.01s || 172 ko | +2.56% | +0.05% 0m00.40s | 430652 ko | Common/List/FlattenList | 0m00.39s | 430684 ko || +0m00.01s || -32 ko | +2.56% | -0.00% 0m00.40s | 432640 ko | Common/Telescope/Equality | 0m00.44s | 432688 ko || -0m00.03s || -48 ko | -9.09% | -0.01% 0m00.39s | 431536 ko | ADTRefinement/Refinements/HoneRepresentation | 0m00.36s | 431588 ko || +0m00.03s || -52 ko | +8.33% | -0.01% 0m00.39s | 420916 ko | Common/BoolFacts | 0m00.36s | 420828 ko || +0m00.03s || 88 ko | +8.33% | +0.02% 0m00.39s | 426592 ko | Common/Enumerable/ReflectiveForall | 0m00.35s | 426500 ko || +0m00.04s || 92 ko | +11.42% | +0.02% 0m00.39s | 422308 ko | Common/Instances | 0m00.40s | 422204 ko || -0m00.01s || 104 ko | -2.50% | +0.02% 0m00.39s | 431664 ko | Common/i3list2 | 0m00.36s | 431676 ko || +0m00.03s || -12 ko | +8.33% | -0.00% 0m00.39s | 431308 ko | Common/ilist | 0m00.39s | 431360 ko || +0m00.00s || -52 ko | +0.00% | -0.01% 0m00.39s | 364768 ko | Parsers/BooleanRecognizerExt | 0m00.37s | 364872 ko || +0m00.02s || -104 ko | +5.40% | -0.02% 0m00.39s | 341128 ko | Parsers/ContextFreeGrammar/Equality | 0m00.42s | 341104 ko || -0m00.02s || 24 ko | -7.14% | +0.00% 0m00.39s | 421712 ko | Parsers/GenericCorrectnessBaseTypes | 0m00.38s | 421808 ko || +0m00.01s || -96 ko | +2.63% | -0.02% 0m00.39s | 445844 ko | Parsers/ParserADTSpecification | 0m00.42s | 445660 ko || -0m00.02s || 184 ko | -7.14% | +0.04% 0m00.39s | 344740 ko | Parsers/Reachable/ParenBalancedHiding/Core | 0m00.38s | 344688 ko || +0m00.01s || 52 ko | +2.63% | +0.01% 0m00.38s | 403712 ko | ADTRefinement/BuildADTSetoidMorphisms | 0m00.37s | 403840 ko || +0m00.01s || -128 ko | +2.70% | -0.03% 0m00.38s | 421508 ko | Common/SetoidInstances | 0m00.36s | 421504 ko || +0m00.02s || 4 ko | +5.55% | +0.00% 0m00.38s | 420904 ko | Common/UIP | 0m00.36s | 420928 ko || +0m00.02s || -24 ko | +5.55% | -0.00% 0m00.38s | 360808 ko | Computation/ApplyMonad | 0m00.38s | 360952 ko || +0m00.00s || -144 ko | +0.00% | -0.03% 0m00.38s | 370600 ko | Parsers/BooleanRecognizerFull | 0m00.33s | 370540 ko || +0m00.04s || 60 ko | +15.15% | +0.01% 0m00.38s | 452276 ko | Parsers/BooleanRecognizerTests | 0m00.39s | 452128 ko || -0m00.01s || 148 ko | -2.56% | +0.03% 0m00.38s | 339312 ko | Parsers/ContextFreeGrammar/PreNotations | 0m00.36s | 339380 ko || +0m00.02s || -68 ko | +5.55% | -0.02% 0m00.38s | 421884 ko | Parsers/ContextFreeGrammar/SimpleTransfer | 0m00.38s | 421496 ko || +0m00.00s || 388 ko | +0.00% | +0.09% 0m00.38s | 409820 ko | Parsers/Reflective/ParserSoundnessOptimized | 0m00.36s | 409936 ko || +0m00.02s || -116 ko | +5.55% | -0.02% 0m00.37s | 409704 ko | Common/Ensembles/Cardinal | 0m00.36s | 409812 ko || +0m00.01s || -108 ko | +2.77% | -0.02% 0m00.37s | 403600 ko | Common/Enumerable/ReflectiveForallStaged | 0m00.33s | 403592 ko || +0m00.03s || 8 ko | +12.12% | +0.00% 0m00.37s | 420572 ko | Common/Le | 0m00.37s | 420396 ko || +0m00.00s || 176 ko | +0.00% | +0.04% 0m00.37s | 394208 ko | Computation/LogicLemmas | 0m00.39s | 394356 ko || -0m00.02s || -148 ko | -5.12% | -0.03% 0m00.37s | 435632 ko | Parsers/Grammars/JSON | 0m00.37s | 435648 ko || +0m00.00s || -16 ko | +0.00% | -0.00% 0m00.37s | 403496 ko | Parsers/Reflective/ParserSemantics | 0m00.38s | 403460 ko || -0m00.01s || 36 ko | -2.63% | +0.00% 0m00.37s | 399756 ko | Parsers/Reflective/ParserSoundness | 0m00.40s | 399652 ko || -0m00.03s || 104 ko | -7.50% | +0.02% 0m00.37s | 415320 ko | Parsers/Reflective/SyntaxEquivalence | 0m00.36s | 415420 ko || +0m00.01s || -100 ko | +2.77% | -0.02% 0m00.36s | 376564 ko | ADT/ADTHide | 0m00.34s | 376704 ko || +0m00.01s || -140 ko | +5.88% | -0.03% 0m00.36s | 373708 ko | ADTInduction | 0m00.38s | 373608 ko || -0m00.02s || 100 ko | -5.26% | +0.02% 0m00.36s | 356704 ko | ADTRefinement/BuildADTRefinements | 0m00.37s | 356636 ko || -0m00.01s || 68 ko | -2.70% | +0.01% 0m00.36s | 412052 ko | ADTRefinement/BuildADTRefinements/AddCache | 0m00.40s | 411996 ko || -0m00.04s || 56 ko | -10.00% | +0.01% 0m00.36s | 377836 ko | ADTRefinement/GeneralBuildADTTactics | 0m00.36s | 377988 ko || +0m00.00s || -152 ko | +0.00% | -0.04% 0m00.36s | 410676 ko | ADTRefinement/Refinements/RefineHideADT | 0m00.37s | 410548 ko || -0m00.01s || 128 ko | -2.70% | +0.03% 0m00.36s | 422336 ko | Common/SetEq | 0m00.37s | 422244 ko || -0m00.01s || 92 ko | -2.70% | +0.02% 0m00.36s | 401196 ko | Common/ilist3_pair | 0m00.32s | 401096 ko || +0m00.03s || 100 ko | +12.49% | +0.02% 0m00.36s | 341528 ko | Parsers/ContextFreeGrammar/TransferProperties | 0m00.37s | 341660 ko || -0m00.01s || -132 ko | -2.70% | -0.03% 0m00.36s | 436028 ko | Parsers/Grammars/JSONImpoverished | 0m00.38s | 435972 ko || -0m00.02s || 56 ko | -5.26% | +0.01% 0m00.36s | 342496 ko | Parsers/ParserInterface | 0m00.36s | 342272 ko || +0m00.00s || 224 ko | +0.00% | +0.06% 0m00.36s | 389112 ko | Parsers/Reflective/ParserSemanticsOptimized | 0m00.38s | 389164 ko || -0m00.02s || -52 ko | -5.26% | -0.01% 0m00.36s | 438144 ko | Parsers/Reflective/PartialUnfold | 0m00.38s | 438108 ko || -0m00.02s || 36 ko | -5.26% | +0.00% 0m00.36s | 349068 ko | Parsers/Reflective/Semantics | 0m00.34s | 349324 ko || +0m00.01s || -256 ko | +5.88% | -0.07% 0m00.36s | 420372 ko | Parsers/StringLike/Core | 0m00.37s | 420368 ko || -0m00.01s || 4 ko | -2.70% | +0.00% 0m00.35s | 387868 ko | ADT/ComputationalADT | 0m00.38s | 387944 ko || -0m00.03s || -76 ko | -7.89% | -0.01% 0m00.35s | 388764 ko | ADTNotation/BuildADTReplaceMethods | 0m00.36s | 388956 ko || -0m00.01s || -192 ko | -2.77% | -0.04% 0m00.35s | 356380 ko | ADTNotation/BuildADTSig | 0m00.33s | 356228 ko || +0m00.01s || 152 ko | +6.06% | +0.04% 0m00.35s | 390024 ko | ADTRefinement/BuildADTRefinements/SimplifyRep | 0m00.34s | 390172 ko || +0m00.00s || -148 ko | +2.94% | -0.03% 0m00.35s | 377536 ko | ADTRefinement/Refinements/SimplifyRep | 0m00.34s | 377404 ko || +0m00.00s || 132 ko | +2.94% | +0.03% 0m00.35s | 422256 ko | Parsers/ContextFreeGrammar/SimpleCorrectnessLemmas | 0m00.35s | 422304 ko || +0m00.00s || -48 ko | +0.00% | -0.01% 0m00.35s | 378764 ko | Parsers/Grammars/ExpressionNumPlusParen | 0m00.35s | 378776 ko || +0m00.00s || -12 ko | +0.00% | -0.00% 0m00.35s | 435848 ko | Parsers/Grammars/JSONImpoverishedOriginal | 0m00.33s | 435892 ko || +0m00.01s || -44 ko | +6.06% | -0.01% 0m00.35s | 336004 ko | Parsers/Reachable/OnlyLast/Reachable | 0m00.33s | 336016 ko || +0m00.01s || -12 ko | +6.06% | -0.00% 0m00.35s | 348660 ko | Parsers/Refinement/PreTactics | 0m00.39s | 348700 ko || -0m00.04s || -40 ko | -10.25% | -0.01% 0m00.34s | 343736 ko | ADT | 0m00.29s | 343592 ko || +0m00.05s || 144 ko | +17.24% | +0.04% 0m00.34s | 402836 ko | ADTNotation/BuildComputationalADT | 0m00.35s | 402764 ko || -0m00.00s || 72 ko | -2.85% | +0.01% 0m00.34s | 300152 ko | Common/EnumType | 0m00.30s | 300100 ko || +0m00.04s || 52 ko | +13.33% | +0.01% 0m00.34s | 398180 ko | Common/Prod | 0m00.34s | 398176 ko || +0m00.00s || 4 ko | +0.00% | +0.00% 0m00.34s | 409800 ko | Common/i2list2 | 0m00.38s | 409948 ko || -0m00.03s || -148 ko | -10.52% | -0.03% 0m00.34s | 359144 ko | Computation/Core | 0m00.33s | 359272 ko || +0m00.01s || -128 ko | +3.03% | -0.03% 0m00.34s | 357476 ko | Computation/FueledFix | 0m00.35s | 357360 ko || -0m00.00s || 116 ko | -2.85% | +0.03% 0m00.34s | 371700 ko | Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretationDefinitionsRelations | 0m00.37s | 371680 ko || -0m00.02s || 20 ko | -8.10% | +0.00% 0m00.34s | 339764 ko | Parsers/ContextFreeGrammar/Notations | 0m00.33s | 339808 ko || +0m00.01s || -44 ko | +3.03% | -0.01% 0m00.34s | 341984 ko | Parsers/ContextFreeGrammar/Precompute | 0m00.37s | 342132 ko || -0m00.02s || -148 ko | -8.10% | -0.04% 0m00.34s | 349932 ko | Parsers/Grammars/ExpressionParen | 0m00.30s | 349816 ko || +0m00.04s || 116 ko | +13.33% | +0.03% 0m00.34s | 335588 ko | Parsers/Reachable/All/Reachable | 0m00.29s | 335492 ko || +0m00.05s || 96 ko | +17.24% | +0.02% 0m00.34s | 335568 ko | Parsers/Reachable/OnlyLast/ReachableWellFounded | 0m00.31s | 335716 ko || +0m00.03s || -148 ko | +9.67% | -0.04% 0m00.34s | 357200 ko | Parsers/Reachable/ParenBalanced/WellFounded | 0m00.33s | 357208 ko || +0m00.01s || -8 ko | +3.03% | -0.00% 0m00.34s | 345384 ko | Parsers/Reflective/ParserPartialUnfold | 0m00.32s | 345324 ko || +0m00.02s || 60 ko | +6.25% | +0.01% 0m00.34s | 352828 ko | Parsers/Reflective/SemanticsOptimized | 0m00.34s | 352640 ko || +0m00.00s || 188 ko | +0.00% | +0.05% 0m00.34s | 377984 ko | Parsers/SimpleRecognizer | 0m00.35s | 377892 ko || -0m00.00s || 92 ko | -2.85% | +0.02% 0m00.33s | 376128 ko | ADT/ADTSig | 0m00.33s | 376128 ko || +0m00.00s || 0 ko | +0.00% | +0.00% 0m00.33s | 348276 ko | ADTRefinement | 0m00.35s | 348204 ko || -0m00.01s || 72 ko | -5.71% | +0.02% 0m00.33s | 347608 ko | ADTRefinement/Refinements | 0m00.33s | 347756 ko || +0m00.00s || -148 ko | +0.00% | -0.04% 0m00.33s | 338824 ko | Computation | 0m00.34s | 338944 ko || -0m00.01s || -120 ko | -2.94% | -0.03% 0m00.33s | 336472 ko | Parsers/ContextFreeGrammar/ReflectiveLemmas | 0m00.37s | 336552 ko || -0m00.03s || -80 ko | -10.81% | -0.02% 0m00.33s | 382328 ko | Parsers/GenericRecognizer | 0m00.32s | 382180 ko || +0m00.01s || 148 ko | +3.12% | +0.03% 0m00.33s | 350840 ko | Parsers/Grammars/ExpressionNumPlus | 0m00.32s | 350876 ko || +0m00.01s || -36 ko | +3.12% | -0.01% 0m00.33s | 355912 ko | Parsers/Grammars/FlatComments | 0m00.32s | 355948 ko || +0m00.01s || -36 ko | +3.12% | -0.01% 0m00.33s | 360684 ko | Parsers/Reachable/ParenBalancedHiding/WellFounded | 0m00.35s | 360816 ko || -0m00.01s || -132 ko | -5.71% | -0.03% 0m00.33s | 348920 ko | Parsers/Reflective/ParserSyntaxEquivalence | 0m00.33s | 348980 ko || +0m00.00s || -60 ko | +0.00% | -0.01% 0m00.33s | 288132 ko | Parsers/Reflective/Reify | 0m00.32s | 288036 ko || +0m00.01s || 96 ko | +3.12% | +0.03% 0m00.33s | 347720 ko | Parsers/StringLike | 0m00.32s | 347684 ko || +0m00.01s || 36 ko | +3.12% | +0.01% 0m00.32s | 383252 ko | Common/Ensembles/Equivalence | 0m00.30s | 383080 ko || +0m00.02s || 172 ko | +6.66% | +0.04% 0m00.32s | 332116 ko | Common/Tactics/CacheStringConstant | 0m00.30s | 332132 ko || +0m00.02s || -16 ko | +6.66% | -0.00% 0m00.32s | 340200 ko | Parsers/ActionEvaluator | 0m00.32s | 340368 ko || +0m00.00s || -168 ko | +0.00% | -0.04% 0m00.32s | 360548 ko | Parsers/BooleanRecognizer | 0m00.31s | 360568 ko || +0m00.01s || -20 ko | +3.22% | -0.00% 0m00.32s | 340008 ko | Parsers/ContextFreeGrammar/PreNotationsLemmas | 0m00.36s | 340276 ko || -0m00.03s || -268 ko | -11.11% | -0.07% 0m00.32s | 378560 ko | Parsers/CorrectnessBaseTypes | 0m00.34s | 378592 ko || -0m00.02s || -32 ko | -5.88% | -0.00% 0m00.32s | 349792 ko | Parsers/Grammars/ABStar | 0m00.35s | 349712 ko || -0m00.02s || 80 ko | -8.57% | +0.02% 0m00.32s | 373876 ko | Parsers/Grammars/EvalGrammarTactics | 0m00.35s | 373960 ko || -0m00.02s || -84 ko | -8.57% | -0.02% 0m00.32s | 365120 ko | Parsers/Grammars/JSComment | 0m00.35s | 365176 ko || -0m00.02s || -56 ko | -8.57% | -0.01% 0m00.32s | 338844 ko | Parsers/Grammars/Trivial | 0m00.36s | 338976 ko || -0m00.03s || -132 ko | -11.11% | -0.03% 0m00.32s | 335452 ko | Parsers/Reachable/MaybeEmpty/Core | 0m00.31s | 335452 ko || +0m00.01s || 0 ko | +3.22% | +0.00% 0m00.32s | 335680 ko | Parsers/Reachable/OnlyFirst/ReachableWellFounded | 0m00.31s | 335696 ko || +0m00.01s || -16 ko | +3.22% | -0.00% 0m00.32s | 280600 ko | Parsers/Reflective/Syntactify | 0m00.33s | 280508 ko || -0m00.01s || 92 ko | -3.03% | +0.03% 0m00.31s | 376756 ko | ADT/Core | 0m00.32s | 376708 ko || -0m00.01s || 48 ko | -3.12% | +0.01% 0m00.31s | 348208 ko | ADTNotation | 0m00.32s | 348108 ko || -0m00.01s || 100 ko | -3.12% | +0.02% 0m00.31s | 391388 ko | ADTRefinement/Core | 0m00.35s | 391332 ko || -0m00.03s || 56 ko | -11.42% | +0.01% 0m00.31s | 385112 ko | ADTRefinement/Refinements/DelegateMethods | 0m00.36s | 385044 ko || -0m00.04s || 68 ko | -13.88% | +0.01% 0m00.31s | 354392 ko | Common/Ensembles | 0m00.32s | 354376 ko || -0m00.01s || 16 ko | -3.12% | +0.00% 0m00.31s | 385940 ko | Common/Monad | 0m00.33s | 385928 ko || -0m00.02s || 12 ko | -6.06% | +0.00% 0m00.31s | 388184 ko | Common/OptionFacts | 0m00.32s | 388212 ko || -0m00.01s || -28 ko | -3.12% | -0.00% 0m00.31s | 390168 ko | Common/Telescope/Instances | 0m00.30s | 390196 ko || +0m00.01s || -28 ko | +3.33% | -0.00% 0m00.31s | 359928 ko | Computation/Refinements/Tactics | 0m00.31s | 359872 ko || +0m00.00s || 56 ko | +0.00% | +0.01% 0m00.31s | 335668 ko | Computation/SetoidEqMorphisms | 0m00.34s | 335420 ko || -0m00.03s || 248 ko | -8.82% | +0.07% 0m00.31s | 355996 ko | Parsers/ContextFreeGrammar/Fix/Inject | 0m00.36s | 356044 ko || -0m00.04s || -48 ko | -13.88% | -0.01% 0m00.31s | 335108 ko | Parsers/Reachable/All/ReachableWellFounded | 0m00.32s | 335188 ko || -0m00.01s || -80 ko | -3.12% | -0.02% 0m00.31s | 334680 ko | Parsers/Reachable/MaybeEmpty/WellFounded | 0m00.31s | 334692 ko || +0m00.00s || -12 ko | +0.00% | -0.00% 0m00.30s | 360100 ko | Common/Ensembles/Tactics | 0m00.30s | 360228 ko || +0m00.00s || -128 ko | +0.00% | -0.03% 0m00.30s | 377288 ko | Common/PointedProp | 0m00.30s | 377156 ko || +0m00.00s || 132 ko | +0.00% | +0.03% 0m00.30s | 370504 ko | Common/StringBound | 0m00.32s | 370428 ko || -0m00.02s || 76 ko | -6.25% | +0.02% 0m00.29s | 370816 ko | Parsers/Grammars/StringLiteral | 0m00.32s | 370612 ko || -0m00.03s || 204 ko | -9.37% | +0.05% 0m00.29s | 336024 ko | Parsers/Reachable/OnlyFirst/Reachable | 0m00.34s | 336036 ko || -0m00.05s || -12 ko | -14.70% | -0.00% 0m00.29s | 330832 ko | Parsers/Specification | 0m00.33s | 330808 ko || -0m00.04s || 24 ko | -12.12% | +0.00% 0m00.28s | 386828 ko | Common/LogicMorphisms | 0m00.27s | 386920 ko || +0m00.01s || -92 ko | +3.70% | -0.02% 0m00.28s | 342456 ko | Parsers/Reflective/ParserSyntax | 0m00.32s | 342304 ko || -0m00.03s || 152 ko | -12.49% | +0.04% 0m00.27s | 385404 ko | Common/SetoidClassInstances | 0m00.29s | 385228 ko || -0m00.01s || 176 ko | -6.89% | +0.04% 0m00.27s | 344108 ko | Parsers/ExtrOcamlPrimitives | 0m00.31s | 344036 ko || -0m00.03s || 72 ko | -12.90% | +0.02% 0m00.27s | 383856 ko | Parsers/GenericBoolCorrectnessBaseTypes | 0m00.29s | 383816 ko || -0m00.01s || 40 ko | -6.89% | +0.01% 0m00.26s | 253600 ko | Common/Coq__8_4__8_5__Compat | 0m00.28s | 253424 ko || -0m00.02s || 176 ko | -7.14% | +0.06% 0m00.25s | 298904 ko | Common/Match | 0m00.24s | 298968 ko || +0m00.01s || -64 ko | +4.16% | -0.02% 0m00.25s | 269740 ko | Common/ReservedNotations | 0m00.24s | 269880 ko || +0m00.01s || -140 ko | +4.16% | -0.05% 0m00.24s | 296800 ko | Common/StringOperations | 0m00.20s | 296772 ko || +0m00.03s || 28 ko | +19.99% | +0.00% 0m00.24s | 274364 ko | Common/Tactics/BreakMatch | 0m00.20s | 274508 ko || +0m00.03s || -144 ko | +19.99% | -0.05% 0m00.24s | 270068 ko | Common/Tactics/Combinators | 0m00.22s | 269980 ko || +0m00.01s || 88 ko | +9.09% | +0.03% 0m00.24s | 270356 ko | Common/Tactics/DestructSig | 0m00.22s | 270444 ko || +0m00.01s || -88 ko | +9.09% | -0.03% 0m00.24s | 270088 ko | Common/Tactics/PrintContext | 0m00.23s | 270080 ko || +0m00.00s || 8 ko | +4.34% | +0.00% 0m00.24s | 338624 ko | Parsers/BaseTypes | 0m00.26s | 338756 ko || -0m00.02s || -132 ko | -7.69% | -0.03% 0m00.24s | 321824 ko | Parsers/ContextFreeGrammar/Core | 0m00.21s | 321816 ko || +0m00.03s || 8 ko | +14.28% | +0.00% 0m00.24s | 269836 ko | Parsers/Grammars/JavaScriptWithoutStatements | 0m00.22s | 269700 ko || +0m00.01s || 136 ko | +9.09% | +0.05% 0m00.24s | 311488 ko | Parsers/WellFoundedParse | 0m00.21s | 311320 ko || +0m00.03s || 168 ko | +14.28% | +0.05% 0m00.23s | 285376 ko | Common/LetIn | 0m00.22s | 285376 ko || +0m00.01s || 0 ko | +4.54% | +0.00% 0m00.23s | 272604 ko | Common/Tactics/DestructHead | 0m00.23s | 272440 ko || +0m00.00s || 164 ko | +0.00% | +0.06% 0m00.23s | 269556 ko | Common/Tactics/GetGoal | 0m00.25s | 269828 ko || -0m00.01s || -272 ko | -7.99% | -0.10% 0m00.23s | 270904 ko | Common/Tactics/SpecializeBy | 0m00.25s | 270816 ko || -0m00.01s || 88 ko | -7.99% | +0.03% 0m00.23s | 300460 ko | Common/Telescope/Core | 0m00.26s | 300436 ko || -0m00.03s || 24 ko | -11.53% | +0.00% 0m00.23s | 279568 ko | Common/VectorFacts | 0m00.22s | 279600 ko || +0m00.01s || -32 ko | +4.54% | -0.01% 0m00.23s | 323688 ko | Parsers/ContextFreeGrammar/SimpleCorrectness | 0m00.25s | 323712 ko || -0m00.01s || -24 ko | -7.99% | -0.00% 0m00.23s | 311136 ko | Parsers/Reachable/MaybeEmpty/Minimal | 0m00.23s | 311104 ko || +0m00.00s || 32 ko | +0.00% | +0.01% 0m00.23s | 314420 ko | Parsers/Reachable/OnlyFirst/MinimalReachable | 0m00.20s | 314448 ko || +0m00.03s || -28 ko | +15.00% | -0.00% 0m00.22s | 270880 ko | Common/Ensembles/Notations | 0m00.21s | 270948 ko || +0m00.01s || -68 ko | +4.76% | -0.02% 0m00.22s | 272076 ko | Common/Tactics/DestructHyps | 0m00.22s | 272072 ko || +0m00.00s || 4 ko | +0.00% | +0.00% 0m00.22s | 269952 ko | Common/Tactics/FoldIsTrue | 0m00.24s | 269892 ko || -0m00.01s || 60 ko | -8.33% | +0.02% 0m00.22s | 270032 ko | Common/Tactics/Head | 0m00.24s | 270016 ko || -0m00.01s || 16 ko | -8.33% | +0.00% 0m00.22s | 269876 ko | Common/Tactics/IsClosed | 0m00.24s | 269832 ko || -0m00.01s || 44 ko | -8.33% | +0.01% 0m00.22s | 273284 ko | Common/Tactics/SetoidSubst | 0m00.24s | 273244 ko || -0m00.01s || 40 ko | -8.33% | +0.01% 0m00.22s | 269860 ko | Computation/Notations | 0m00.22s | 269860 ko || +0m00.00s || 0 ko | +0.00% | +0.00% 0m00.22s | 321044 ko | Parsers/ContextFreeGrammar/Transfer | 0m00.23s | 320924 ko || -0m00.01s || 120 ko | -4.34% | +0.03% 0m00.22s | 300944 ko | Parsers/ContextFreeGrammar/Valid | 0m00.21s | 300960 ko || +0m00.01s || -16 ko | +4.76% | -0.00% 0m00.22s | 300092 ko | Parsers/GenericBaseTypes | 0m00.21s | 300052 ko || +0m00.01s || 40 ko | +4.76% | +0.01% 0m00.22s | 269740 ko | Parsers/Grammars/JavaScriptExpression | 0m00.22s | 269748 ko || +0m00.00s || -8 ko | +0.00% | -0.00% 0m00.22s | 328336 ko | Parsers/MinimalParse | 0m00.25s | 328352 ko || -0m00.03s || -16 ko | -12.00% | -0.00% 0m00.22s | 269964 ko | Parsers/Refinement/DisjointRulesCommon | 0m00.22s | 269964 ko || +0m00.00s || 0 ko | +0.00% | +0.00% 0m00.21s | 269832 ko | Common/Tactics/FreeIn | 0m00.22s | 269840 ko || -0m00.01s || -8 ko | -4.54% | -0.00% 0m00.21s | 270920 ko | Common/Tactics/SplitInContext | 0m00.24s | 270956 ko || -0m00.03s || -36 ko | -12.50% | -0.01% 0m00.21s | 312912 ko | Parsers/Reachable/All/MinimalReachable | 0m00.23s | 313024 ko || -0m00.02s || -112 ko | -8.69% | -0.03% 0m00.21s | 314448 ko | Parsers/Reachable/OnlyLast/MinimalReachable | 0m00.23s | 314548 ko || -0m00.02s || -100 ko | -8.69% | -0.03% 0m00.21s | 269788 ko | Parsers/Refinement/DisjointLemmasEarlyDeclarations | 0m00.24s | 269756 ko || -0m00.03s || 32 ko | -12.50% | +0.01% 0m00.20s | 269228 ko | Parsers/BooleanRecognizerMin | 0m00.22s | 269192 ko || -0m00.01s || 36 ko | -9.09% | +0.01% 0m00.20s | 269828 ko | Parsers/Grammars/JavaScriptStatementsWithoutAssignmentExpression | 0m00.22s | 269604 ko || -0m00.01s || 224 ko | -9.09% | +0.08% 0m00.19s | 271456 ko | Common/Notations | 0m00.22s | 271340 ko || -0m00.03s || 116 ko | -13.63% | +0.04% 0m00.05s | 60308 ko | Common/Tactics/HintDbExtra | 0m00.03s | 60136 ko || +0m00.02s || 172 ko | +66.66% | +0.28% 0m00.04s | 60508 ko | Common/Tactics/TransparentAbstract | 0m00.04s | 60436 ko || +0m00.00s || 72 ko | +0.00% | +0.11% 0m00.03s | 15736 ko | Common/Tactics/transparent_abstract_plugin | 0m00.02s | 15816 ko || +0m00.00s || -80 ko | +49.99% | -0.50% 0m00.02s | 15672 ko | Common/Tactics/hint_db_extra_plugin | 0m00.03s | 15624 ko || -0m00.00s || 48 ko | -33.33% | +0.30% 0m00.02s | 23376 ko | Common/Tactics/hint_db_extra_tactics | 0m00.03s | 23256 ko || -0m00.00s || 120 ko | -33.33% | +0.51% 0m00.01s | 22016 ko | Common/Tactics/transparent_abstract_tactics | 0m00.02s | 22032 ko || -0m00.01s || -16 ko | -50.00% | -0.07% ```

Diff between 21bc38e31e498465854e57eb8bc791523f100c4e (after) and 395460462593193233975c071133dd9cab876939 (before)

``` 21bc38e | Peak Mem | File Name | 3954604 | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ 7m33.37s | 871544 ko | Total Time / Peak Mem | 7m33.62s | 871524 ko || -0m00.25s || 20 ko | -0.05% | +0.00% ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ 0m03.79s | 499448 ko | Parsers/ContextFreeGrammar/Fix/FixRelated | 0m04.89s | 499400 ko || -0m01.09s || 48 ko | -22.49% | +0.00% 0m22.95s | 739528 ko | Parsers/ParserFromParserADT | 0m22.99s | 739404 ko || -0m00.03s || 124 ko | -0.17% | +0.01% 0m21.84s | 694412 ko | Parsers/GenericRecognizerMin | 0m21.83s | 694420 ko || +0m00.01s || -8 ko | +0.04% | -0.00% 0m20.75s | 597996 ko | Parsers/Refinement/PossibleTerminalsSets | 0m20.94s | 597468 ko || -0m00.19s || 528 ko | -0.90% | +0.08% 0m19.71s | 871544 ko | Parsers/BooleanRecognizerOptimized | 0m19.77s | 871524 ko || -0m00.05s || 20 ko | -0.30% | +0.00% 0m16.44s | 816344 ko | Parsers/BooleanRecognizerOptimizedReflectiveCorrectness | 0m16.09s | 816256 ko || +0m00.35s || 88 ko | +2.17% | +0.01% 0m16.05s | 800008 ko | Parsers/GenericRecognizerOptimized | 0m15.83s | 795452 ko || +0m00.22s || 4556 ko | +1.38% | +0.57% 0m14.26s | 571240 ko | Parsers/SplitterFromParserADT | 0m14.15s | 571080 ko || +0m00.10s || 160 ko | +0.77% | +0.02% 0m10.91s | 479988 ko | Common/FMapExtensions | 0m10.93s | 480164 ko || -0m00.01s || -176 ko | -0.18% | -0.03% 0m10.71s | 466752 ko | Parsers/Refinement/BinOpBrackets/MakeBinOpTable | 0m10.88s | 466700 ko || -0m00.16s || 52 ko | -1.56% | +0.01% 0m10.25s | 796260 ko | Parsers/Reflective/LogicalRelations | 0m10.28s | 796332 ko || -0m00.02s || -72 ko | -0.29% | -0.00% 0m09.06s | 636068 ko | Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflective | 0m09.41s | 635928 ko || -0m00.34s || 140 ko | -3.71% | +0.02% 0m07.52s | 512184 ko | Parsers/ContextFreeGrammar/Fix/Fix | 0m07.46s | 511744 ko || +0m00.05s || 440 ko | +0.80% | +0.08% 0m06.09s | 469896 ko | Common/List/ListFacts | 0m06.15s | 470016 ko || -0m00.06s || -120 ko | -0.97% | -0.02% 0m05.55s | 546748 ko | Parsers/StringLike/LastChar | 0m05.30s | 551376 ko || +0m00.25s || -4628 ko | +4.71% | -0.83% 0m04.80s | 506948 ko | Parsers/MinimalParseOfParse | 0m04.82s | 506916 ko || -0m00.02s || 32 ko | -0.41% | +0.00% 0m04.73s | 445264 ko | Parsers/StringLike/Properties | 0m04.69s | 445176 ko || +0m00.04s || 88 ko | +0.85% | +0.01% 0m04.57s | 569940 ko | Parsers/Refinement/DisjointRulesRev | 0m04.57s | 569860 ko || +0m00.00s || 80 ko | +0.00% | +0.01% 0m04.46s | 441544 ko | Parsers/StringLike/FirstCharSuchThat | 0m04.56s | 441504 ko || -0m00.09s || 40 ko | -2.19% | +0.00% 0m04.36s | 452608 ko | Parsers/Grammars/Tests | 0m04.29s | 452720 ko || +0m00.07s || -112 ko | +1.63% | -0.02% 0m04.29s | 488724 ko | Parsers/Grammars/JSONTests | 0m04.31s | 488716 ko || -0m00.01s || 8 ko | -0.46% | +0.00% 0m04.28s | 509420 ko | Parsers/StringLike/OcamlString | 0m04.32s | 509220 ko || -0m00.04s || 200 ko | -0.92% | +0.03% 0m03.97s | 558136 ko | Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflectiveOpt | 0m03.79s | 558180 ko || +0m00.18s || -44 ko | +4.74% | -0.00% 0m03.87s | 451248 ko | Parsers/AbstractInterpretation/NonTerminalMap | 0m04.04s | 451448 ko || -0m00.16s || -200 ko | -4.20% | -0.04% 0m03.64s | 460452 ko | Parsers/ContextFreeGrammar/Fix/ProdAbstractInterpretationDefinitions | 0m03.59s | 460212 ko || +0m00.05s || 240 ko | +1.39% | +0.05% 0m03.53s | 440704 ko | Common/Ensembles/IndexedEnsembles | 0m03.52s | 440696 ko || +0m00.00s || 8 ko | +0.28% | +0.00% 0m03.52s | 580480 ko | Parsers/Refinement/DisjointRules | 0m03.70s | 580392 ko || -0m00.18s || 88 ko | -4.86% | +0.01% 0m03.47s | 476932 ko | Common/FMapExtensions/LiftRelationInstances | 0m03.46s | 477040 ko || +0m00.01s || -108 ko | +0.28% | -0.02% 0m03.30s | 506048 ko | Parsers/BooleanRecognizerOptimizedReflective | 0m03.31s | 506076 ko || -0m00.01s || -28 ko | -0.30% | -0.00% 0m03.27s | 454148 ko | Parsers/Grammars/JavaScript | 0m03.21s | 454104 ko || +0m00.06s || 44 ko | +1.86% | +0.00% 0m03.05s | 441072 ko | Parsers/Refinement/BinOpBrackets/ParenBalancedLemmas | 0m03.03s | 440836 ko || +0m00.02s || 236 ko | +0.66% | +0.05% 0m02.99s | 467212 ko | Parsers/SimpleRecognizerCorrect | 0m02.87s | 467900 ko || +0m00.12s || -688 ko | +4.18% | -0.14% 0m02.84s | 592268 ko | Parsers/Refinement/SharpenedJSComment | 0m02.84s | 592332 ko || +0m00.00s || -64 ko | +0.00% | -0.01% 0m02.81s | 462268 ko | Common/Wf2 | 0m02.80s | 462384 ko || +0m00.01s || -116 ko | +0.35% | -0.02% 0m02.81s | 445700 ko | Parsers/GenericRecognizerExt | 0m02.86s | 445820 ko || -0m00.04s || -120 ko | -1.74% | -0.02% 0m02.77s | 452928 ko | Parsers/Refinement/FinishingLemma | 0m02.73s | 452860 ko || +0m00.04s || 68 ko | +1.46% | +0.01% 0m02.72s | 496812 ko | Parsers/Refinement/EmptyLemmas | 0m02.72s | 496736 ko || +0m00.00s || 76 ko | +0.00% | +0.01% 0m02.67s | 497136 ko | Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretation | 0m02.63s | 499716 ko || +0m00.04s || -2580 ko | +1.52% | -0.51% 0m02.66s | 492196 ko | Common/FMapExtensions/Wf | 0m02.62s | 492152 ko || +0m00.04s || 44 ko | +1.52% | +0.00% 0m02.55s | 496220 ko | Parsers/Refinement/FixedLengthLemmas | 0m02.49s | 496196 ko || +0m00.05s || 24 ko | +2.40% | +0.00% 0m02.49s | 631064 ko | Parsers/Refinement/SharpenedExpressionPlus | 0m02.51s | 631124 ko || -0m00.01s || -60 ko | -0.79% | -0.00% 0m02.41s | 445216 ko | Parsers/Refinement/BinOpBrackets/ParenBalancedGrammar | 0m02.49s | 445048 ko || -0m00.08s || 168 ko | -3.21% | +0.03% 0m02.40s | 585048 ko | Parsers/Refinement/BinOpBrackets/BinOpRules | 0m02.38s | 585060 ko || +0m00.02s || -12 ko | +0.84% | -0.00% 0m02.35s | 634812 ko | Parsers/Refinement/SharpenedExpressionPlusParen | 0m02.34s | 634832 ko || +0m00.01s || -20 ko | +0.42% | -0.00% 0m02.34s | 444684 ko | Parsers/ContextFreeGrammar/Fix/Prod | 0m02.30s | 444728 ko || +0m00.04s || -44 ko | +1.73% | -0.00% 0m02.25s | 438288 ko | Parsers/StringLike/ForallChars | 0m02.36s | 438480 ko || -0m00.10s || -192 ko | -4.66% | -0.04% 0m02.12s | 444676 ko | Parsers/Refinement/BinOpBrackets/ParenBalanced | 0m02.04s | 444784 ko || +0m00.08s || -108 ko | +3.92% | -0.02% 0m02.10s | 496696 ko | Parsers/ContextFreeGrammar/Fix/Correct | 0m01.98s | 496800 ko || +0m00.12s || -104 ko | +6.06% | -0.02% 0m02.05s | 439152 ko | Parsers/Splitters/RDPList | 0m02.04s | 439196 ko || +0m00.00s || -44 ko | +0.49% | -0.01% 0m01.99s | 452420 ko | ADTRefinement/FixedPoint | 0m01.92s | 452560 ko || +0m00.07s || -140 ko | +3.64% | -0.03% 0m01.95s | 582120 ko | Parsers/Refinement/SharpenedStringLiteral | 0m01.95s | 581664 ko || +0m00.00s || 456 ko | +0.00% | +0.07% 0m01.90s | 437984 ko | Common/List/ListMorphisms | 0m01.93s | 437908 ko || -0m00.03s || 76 ko | -1.55% | +0.01% 0m01.90s | 443100 ko | Computation/Refinements/General | 0m01.89s | 443036 ko || +0m00.01s || 64 ko | +0.52% | +0.01% 0m01.83s | 440852 ko | Parsers/StringLike/LastCharSuchThat | 0m01.80s | 440848 ko || +0m00.03s || 4 ko | +1.66% | +0.00% 0m01.74s | 431844 ko | Common/BoundedLookup | 0m01.80s | 431784 ko || -0m00.06s || 60 ko | -3.33% | +0.01% 0m01.74s | 432468 ko | Common/Frame | 0m01.71s | 432404 ko || +0m00.03s || 64 ko | +1.75% | +0.01% 0m01.70s | 441800 ko | Common/Wf1 | 0m01.66s | 441792 ko || +0m00.04s || 8 ko | +2.40% | +0.00% 0m01.66s | 437100 ko | Common/Ensembles/EnsembleListEquivalence | 0m01.63s | 437024 ko || +0m00.03s || 76 ko | +1.84% | +0.01% 0m01.64s | 450956 ko | Parsers/RecognizerPreOptimized | 0m01.64s | 451092 ko || +0m00.00s || -136 ko | +0.00% | -0.03% 0m01.61s | 627588 ko | Parsers/Refinement/SharpenedExpressionPlusParenParseTree | 0m01.61s | 627688 ko || +0m00.00s || -100 ko | +0.00% | -0.01% 0m01.59s | 448500 ko | Parsers/GenericRecognizerBoolEquality | 0m01.58s | 448436 ko || +0m00.01s || 64 ko | +0.63% | +0.01% 0m01.58s | 443468 ko | Common/StringFacts | 0m01.59s | 443372 ko || -0m00.01s || 96 ko | -0.62% | +0.02% 0m01.55s | 437984 ko | Common | 0m01.50s | 437976 ko || +0m00.05s || 8 ko | +3.33% | +0.00% 0m01.55s | 573544 ko | Parsers/Refinement/SharpenedABStar | 0m01.55s | 573596 ko || +0m00.00s || -52 ko | +0.00% | -0.00% 0m01.46s | 441584 ko | Parsers/StringLike/FirstChar | 0m01.42s | 441680 ko || +0m00.04s || -96 ko | +2.81% | -0.02% 0m01.45s | 455968 ko | Parsers/Reachable/ParenBalancedHiding/MinimalOfCore | 0m01.43s | 455860 ko || +0m00.02s || 108 ko | +1.39% | +0.02% 0m01.40s | 464092 ko | Parsers/Reflective/SyntaxEquality | 0m01.40s | 464040 ko || +0m00.00s || 52 ko | +0.00% | +0.01% 0m01.39s | 570852 ko | Parsers/Refinement/SharpenedExpressionParen | 0m01.42s | 570880 ko || -0m00.03s || -28 ko | -2.11% | -0.00% 0m01.36s | 438740 ko | Parsers/Reflective/SyntaxEquivalenceReflective | 0m01.33s | 438640 ko || +0m00.03s || 100 ko | +2.25% | +0.02% 0m01.26s | 448304 ko | Parsers/Grammars/JavaScriptAssignmentExpression | 0m01.28s | 448472 ko || -0m00.02s || -168 ko | -1.56% | -0.03% 0m01.23s | 442552 ko | Common/List/PermutationFacts | 0m01.23s | 442480 ko || +0m00.00s || 72 ko | +0.00% | +0.01% 0m01.16s | 430236 ko | Common/DecideableEnsembles | 0m01.18s | 430212 ko || -0m00.02s || 24 ko | -1.69% | +0.00% 0m01.15s | 443196 ko | Computation/FixComp | 0m01.17s | 443036 ko || -0m00.02s || 160 ko | -1.70% | +0.03% 0m01.14s | 451776 ko | Parsers/Reachable/ParenBalanced/MinimalOfCore | 0m01.23s | 451880 ko || -0m00.09s || -104 ko | -7.31% | -0.02% 0m01.10s | 486808 ko | Parsers/ContextFreeGrammar/Fix/AsciiLattice | 0m01.07s | 486712 ko || +0m00.03s || 96 ko | +2.80% | +0.01% 0m01.09s | 456640 ko | Parsers/Splitters/BruteForce | 0m01.09s | 457168 ko || +0m00.00s || -528 ko | +0.00% | -0.11% 0m01.08s | 436552 ko | Common/Enumerable/ReflectiveForallAggregate | 0m01.06s | 436528 ko || +0m00.02s || 24 ko | +1.88% | +0.00% 0m01.08s | 564728 ko | Parsers/Refinement/DisjointLemmas | 0m01.09s | 564632 ko || -0m00.01s || 96 ko | -0.91% | +0.01% 0m01.04s | 437724 ko | Common/NatFacts | 0m01.04s | 437756 ko || +0m00.00s || -32 ko | +0.00% | -0.00% 0m01.01s | 436408 ko | Common/SetEqProperties | 0m01.02s | 436388 ko || -0m00.01s || 20 ko | -0.98% | +0.00% 0m01.01s | 454664 ko | Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretationDefinitions | 0m01.04s | 454608 ko || -0m00.03s || 56 ko | -2.88% | +0.01% 0m01.00s | 448648 ko | Computation/Refinements/Iterate_Decide_Comp | 0m00.99s | 448696 ko || +0m00.01s || -48 ko | +1.01% | -0.01% 0m00.99s | 443164 ko | Common/MSetExtensions | 0m01.00s | 443132 ko || -0m00.01s || 32 ko | -1.00% | +0.00% 0m00.99s | 444244 ko | Parsers/ContextFreeGrammar/Fix/Properties | 0m00.90s | 444176 ko || +0m00.08s || 68 ko | +9.99% | +0.01% 0m00.98s | 452280 ko | Common/MSetBoundedLattice | 0m01.03s | 451468 ko || -0m00.05s || 812 ko | -4.85% | +0.17% 0m00.98s | 437772 ko | Parsers/StringLike/String | 0m00.98s | 437876 ko || +0m00.00s || -104 ko | +0.00% | -0.02% 0m00.97s | 469388 ko | Parsers/ParserImplementation | 0m01.06s | 469416 ko || -0m00.09s || -28 ko | -8.49% | -0.00% 0m00.96s | 431296 ko | Common/Ensembles/CombinatorLaws | 0m00.95s | 431352 ko || +0m00.01s || -56 ko | +1.05% | -0.01% 0m00.95s | 433128 ko | Common/Equality | 0m00.97s | 433048 ko || -0m00.02s || 80 ko | -2.06% | +0.01% 0m00.94s | 435268 ko | Computation/IfDec | 0m00.90s | 435196 ko || +0m00.03s || 72 ko | +4.44% | +0.01% 0m00.93s | 431732 ko | Computation/SetoidMorphisms | 0m00.93s | 431656 ko || +0m00.00s || 76 ko | +0.00% | +0.01% 0m00.92s | 450852 ko | Parsers/Reachable/ParenBalanced/OfParse | 0m00.91s | 450760 ko || +0m00.01s || 92 ko | +1.09% | +0.02% 0m00.91s | 540424 ko | Parsers/ContextFreeGrammar/ExplorationUtil | 0m00.89s | 540460 ko || +0m00.02s || -36 ko | +2.24% | -0.00% 0m00.84s | 508136 ko | Parsers/AbstractInterpretation/NonTerminalMapWf | 0m00.86s | 508196 ko || -0m00.02s || -60 ko | -2.32% | -0.01% 0m00.84s | 572392 ko | Parsers/Refinement/Tactics | 0m00.83s | 572280 ko || +0m00.01s || 112 ko | +1.20% | +0.01% 0m00.83s | 442364 ko | ADTRefinement/BuildADTRefinements/HoneRepresentation | 0m00.80s | 442156 ko || +0m00.02s || 208 ko | +3.74% | +0.04% 0m00.83s | 436056 ko | ADTRefinement/SetoidMorphisms | 0m00.84s | 436116 ko || -0m00.01s || -60 ko | -1.19% | -0.01% 0m00.82s | 438544 ko | Common/Enumerable | 0m00.78s | 438468 ko || +0m00.03s || 76 ko | +5.12% | +0.01% 0m00.79s | 564200 ko | Parsers/Refinement/ExtractSharpenedABStar | 0m00.65s | 564160 ko || +0m00.14s || 40 ko | +21.53% | +0.00% 0m00.77s | 566944 ko | Parsers/Refinement/SharpenedABStarParseTree | 0m00.79s | 567004 ko || -0m00.02s || -60 ko | -2.53% | -0.01% 0m00.75s | 428740 ko | Computation/Decidable | 0m00.76s | 428888 ko || -0m00.01s || -148 ko | -1.31% | -0.03% 0m00.71s | 435096 ko | Common/IterateBoundedIndex | 0m00.71s | 435172 ko || +0m00.00s || -76 ko | +0.00% | -0.01% 0m00.71s | 443596 ko | Computation/ListComputations | 0m00.73s | 443572 ko || -0m00.02s || 24 ko | -2.73% | +0.00% 0m00.69s | 566256 ko | Parsers/ExtrOcamlParsers | 0m00.71s | 566276 ko || -0m00.02s || -20 ko | -2.81% | -0.00% 0m00.69s | 437556 ko | Parsers/Reachable/MaybeEmpty/MinimalOfCore | 0m00.67s | 437640 ko || +0m00.01s || -84 ko | +2.98% | -0.01% 0m00.69s | 438716 ko | Parsers/Reachable/OnlyLast/MinimalReachableOfReachable | 0m00.68s | 438668 ko || +0m00.00s || 48 ko | +1.47% | +0.01% 0m00.68s | 437324 ko | Common/List/UpperBound | 0m00.67s | 437296 ko || +0m00.01s || 28 ko | +1.49% | +0.00% 0m00.68s | 428912 ko | Common/Wf | 0m00.68s | 429096 ko || +0m00.00s || -184 ko | +0.00% | -0.04% 0m00.67s | 432580 ko | Computation/FoldComp | 0m00.65s | 432508 ko || +0m00.02s || 72 ko | +3.07% | +0.01% 0m00.67s | 437348 ko | Parsers/Reachable/All/MinimalReachableOfReachable | 0m00.65s | 437492 ko || +0m00.02s || -144 ko | +3.07% | -0.03% 0m00.66s | 431364 ko | Common/Ensembles/Morphisms | 0m00.65s | 431324 ko || +0m00.01s || 40 ko | +1.53% | +0.00% 0m00.66s | 440512 ko | Parsers/ContextFreeGrammar/Fix/Definitions | 0m00.66s | 440424 ko || +0m00.00s || 88 ko | +0.00% | +0.01% 0m00.66s | 444208 ko | Parsers/ContextFreeGrammar/ValidProperties | 0m00.71s | 444224 ko || -0m00.04s || -16 ko | -7.04% | -0.00% 0m00.65s | 483580 ko | Parsers/SimpleRecognizerOptimized | 0m00.65s | 483588 ko || +0m00.00s || -8 ko | +0.00% | -0.00% 0m00.63s | 438672 ko | Parsers/Reachable/OnlyFirst/MinimalReachableOfReachable | 0m00.65s | 438672 ko || -0m00.02s || 0 ko | -3.07% | +0.00% 0m00.62s | 443884 ko | Parsers/ContextFreeGrammar/Fold | 0m00.63s | 444048 ko || -0m00.01s || -164 ko | -1.58% | -0.03% 0m00.61s | 442664 ko | Parsers/ContextFreeGrammar/ValidReflective | 0m00.61s | 442804 ko || +0m00.00s || -140 ko | +0.00% | -0.03% 0m00.60s | 438608 ko | Parsers/ContextFreeGrammar/Properties | 0m00.62s | 438380 ko || -0m00.02s || 228 ko | -3.22% | +0.05% 0m00.60s | 444424 ko | Parsers/Reachable/OnlyLast/ReachableParse | 0m00.59s | 444368 ko || +0m00.01s || 56 ko | +1.69% | +0.01% 0m00.58s | 441212 ko | ADTRefinement/Refinements/ADTCache | 0m00.62s | 441160 ko || -0m00.04s || 52 ko | -6.45% | +0.01% 0m00.58s | 441832 ko | Parsers/Reflective/Syntax | 0m00.57s | 441924 ko || +0m00.01s || -92 ko | +1.75% | -0.02% 0m00.57s | 436168 ko | Parsers/ContextFreeGrammar/SimpleCorrectnessMorphisms | 0m00.53s | 436168 ko || +0m00.03s || 0 ko | +7.54% | +0.00% 0m00.56s | 440132 ko | ADTNotation/BuildADT | 0m00.61s | 439996 ko || -0m00.04s || 136 ko | -8.19% | +0.03% 0m00.56s | 434096 ko | Common/SumType | 0m00.59s | 434172 ko || -0m00.02s || -76 ko | -5.08% | -0.01% 0m00.56s | 438944 ko | Parsers/ContextFreeGrammar/Carriers | 0m00.54s | 438884 ko || +0m00.02s || 60 ko | +3.70% | +0.01% 0m00.56s | 448932 ko | Parsers/GenericRecognizerEquality | 0m00.55s | 448904 ko || +0m00.01s || 28 ko | +1.81% | +0.00% 0m00.55s | 420088 ko | Parsers/ContextFreeGrammar/Fix/PreInterface | 0m00.57s | 419800 ko || -0m00.01s || 288 ko | -3.50% | +0.06% 0m00.55s | 445196 ko | Parsers/Reachable/All/ReachableParse | 0m00.47s | 445408 ko || +0m00.08s || -212 ko | +17.02% | -0.04% 0m00.54s | 431844 ko | Common/i3list | 0m00.56s | 431656 ko || -0m00.02s || 188 ko | -3.57% | +0.04% 0m00.54s | 496352 ko | Parsers/ParserImplementationOptimized | 0m00.55s | 496088 ko || -0m00.01s || 264 ko | -1.81% | +0.05% 0m00.54s | 458060 ko | Parsers/Reflective/ParserLogicalRelations | 0m00.54s | 458008 ko || +0m00.00s || 52 ko | +0.00% | +0.01% 0m00.53s | 438964 ko | ADTRefinement/GeneralRefinements | 0m00.55s | 438864 ko || -0m00.02s || 100 ko | -3.63% | +0.02% 0m00.53s | 492492 ko | Parsers/ContextFreeGrammar/Fix/Interface | 0m00.53s | 492472 ko || +0m00.00s || 20 ko | +0.00% | +0.00% 0m00.53s | 437672 ko | Parsers/Reachable/ParenBalanced/Core | 0m00.56s | 437684 ko || -0m00.03s || -12 ko | -5.35% | -0.00% 0m00.52s | 441420 ko | ADTRefinement/GeneralBuildADTRefinements | 0m00.46s | 441452 ko || +0m00.06s || -32 ko | +13.04% | -0.00% 0m00.52s | 422228 ko | Common/String_as_OT | 0m00.52s | 422260 ko || +0m00.00s || -32 ko | +0.00% | -0.00% 0m00.50s | 442604 ko | ADTRefinement/BuildADTRefinements/RefineAllMethods | 0m00.47s | 442700 ko || +0m00.03s || -96 ko | +6.38% | -0.02% 0m00.50s | 460264 ko | Parsers/BooleanRecognizerCorrect | 0m00.48s | 460240 ko || +0m00.02s || 24 ko | +4.16% | +0.00% 0m00.48s | 432412 ko | Common/ilist2 | 0m00.49s | 432568 ko || -0m00.01s || -156 ko | -2.04% | -0.03% 0m00.48s | 428248 ko | Parsers/GenericRecognizerOptimizedTactics | 0m00.46s | 428348 ko || +0m00.01s || -100 ko | +4.34% | -0.02% 0m00.48s | 443560 ko | Parsers/Reflective/Morphisms | 0m00.51s | 443640 ko || -0m00.03s || -80 ko | -5.88% | -0.01% 0m00.48s | 443380 ko | Parsers/WellFoundedParseProperties | 0m00.50s | 443272 ko || -0m00.02s || 108 ko | -4.00% | +0.02% 0m00.47s | 435388 ko | Common/FixedPoints | 0m00.46s | 435576 ko || +0m00.00s || -188 ko | +2.17% | -0.04% 0m00.47s | 400268 ko | Parsers/GenericRecognizerCorrect | 0m00.44s | 400304 ko || +0m00.02s || -36 ko | +6.81% | -0.00% 0m00.47s | 416456 ko | Parsers/Reachable/OnlyFirst/ReachableParse | 0m00.46s | 416508 ko || +0m00.00s || -52 ko | +2.17% | -0.01% 0m00.47s | 506172 ko | Parsers/Refinement/ReductionTactics | 0m00.45s | 506332 ko || +0m00.01s || -160 ko | +4.44% | -0.03% 0m00.45s | 438976 ko | ADTRefinement/Refinements/ADTRepInv | 0m00.45s | 438848 ko || +0m00.00s || 128 ko | +0.00% | +0.02% 0m00.45s | 420536 ko | Common/LogicFacts | 0m00.46s | 420388 ko || -0m00.01s || 148 ko | -2.17% | +0.03% 0m00.45s | 446204 ko | Parsers/BooleanRecognizerEquality | 0m00.46s | 446168 ko || -0m00.01s || 36 ko | -2.17% | +0.00% 0m00.44s | 341224 ko | Parsers/ContextFreeGrammar/Equality | 0m00.39s | 341128 ko || +0m00.04s || 96 ko | +12.82% | +0.02% 0m00.44s | 445652 ko | Parsers/ParserADTSpecification | 0m00.39s | 445844 ko || +0m00.04s || -192 ko | +12.82% | -0.04% 0m00.43s | 435440 ko | Common/List/DisjointFacts | 0m00.45s | 435632 ko || -0m00.02s || -192 ko | -4.44% | -0.04% 0m00.42s | 430656 ko | Common/List/FlattenList | 0m00.40s | 430652 ko || +0m00.01s || 4 ko | +4.99% | +0.00% 0m00.42s | 433400 ko | Common/List/Operations | 0m00.41s | 433520 ko || +0m00.01s || -120 ko | +2.43% | -0.02% 0m00.42s | 432716 ko | Common/Telescope/Equality | 0m00.40s | 432640 ko || +0m00.01s || 76 ko | +4.99% | +0.01% 0m00.42s | 452108 ko | Parsers/BooleanRecognizerTests | 0m00.38s | 452276 ko || +0m00.03s || -168 ko | +10.52% | -0.03% 0m00.42s | 441816 ko | Parsers/Reachable/MaybeEmpty/OfParse | 0m00.49s | 441876 ko || -0m00.07s || -60 ko | -14.28% | -0.01% 0m00.41s | 433368 ko | Common/Sigma | 0m00.42s | 433444 ko || -0m00.01s || -76 ko | -2.38% | -0.01% 0m00.41s | 364660 ko | Parsers/BooleanRecognizerExt | 0m00.39s | 364768 ko || +0m00.01s || -108 ko | +5.12% | -0.02% 0m00.41s | 381792 ko | Parsers/SimpleBooleanRecognizerEquality | 0m00.45s | 381908 ko || -0m00.04s || -116 ko | -8.88% | -0.03% 0m00.41s | 365036 ko | Parsers/SimpleRecognizerExt | 0m00.42s | 365056 ko || -0m00.01s || -20 ko | -2.38% | -0.00% 0m00.40s | 420924 ko | Common/BoolFacts | 0m00.39s | 420916 ko || +0m00.01s || 8 ko | +2.56% | +0.00% 0m00.40s | 432432 ko | Common/Gensym | 0m00.43s | 432320 ko || -0m00.02s || 112 ko | -6.97% | +0.02% 0m00.40s | 431380 ko | Common/ilist | 0m00.39s | 431308 ko || +0m00.01s || 72 ko | +2.56% | +0.01% 0m00.40s | 360616 ko | Computation/Monad | 0m00.43s | 360636 ko || -0m00.02s || -20 ko | -6.97% | -0.00% 0m00.40s | 421628 ko | Parsers/ContextFreeGrammar/SimpleTransfer | 0m00.38s | 421884 ko || +0m00.02s || -256 ko | +5.26% | -0.06% 0m00.40s | 435852 ko | Parsers/Grammars/JSONImpoverished | 0m00.36s | 436028 ko || +0m00.04s || -176 ko | +11.11% | -0.04% 0m00.40s | 445392 ko | Parsers/ParserInterfaceReflective | 0m00.44s | 445616 ko || -0m00.03s || -224 ko | -9.09% | -0.05% 0m00.40s | 348752 ko | Parsers/Refinement/PreTactics | 0m00.35s | 348660 ko || +0m00.05s || 92 ko | +14.28% | +0.02% 0m00.40s | 399780 ko | Parsers/Reflective/ParserSoundness | 0m00.37s | 399756 ko || +0m00.03s || 24 ko | +8.10% | +0.00% 0m00.39s | 387864 ko | ADT/ComputationalADT | 0m00.35s | 387868 ko || +0m00.04s || -4 ko | +11.42% | -0.00% 0m00.39s | 373596 ko | ADTInduction | 0m00.36s | 373708 ko || +0m00.03s || -112 ko | +8.33% | -0.02% 0m00.39s | 341836 ko | Common/Enumerable/BoolProp | 0m00.40s | 341868 ko || -0m00.01s || -32 ko | -2.50% | -0.00% 0m00.39s | 360940 ko | Computation/ApplyMonad | 0m00.38s | 360808 ko || +0m00.01s || 132 ko | +2.63% | +0.03% 0m00.39s | 367976 ko | Parsers/ContextFreeGrammar/Reflective | 0m00.42s | 368128 ko || -0m00.02s || -152 ko | -7.14% | -0.04% 0m00.39s | 421800 ko | Parsers/GenericCorrectnessBaseTypes | 0m00.39s | 421712 ko || +0m00.00s || 88 ko | +0.00% | +0.02% 0m00.39s | 403464 ko | Parsers/Reflective/ParserSemantics | 0m00.37s | 403496 ko || +0m00.02s || -32 ko | +5.40% | -0.00% 0m00.39s | 389112 ko | Parsers/Reflective/ParserSemanticsOptimized | 0m00.36s | 389112 ko || +0m00.03s || 0 ko | +8.33% | +0.00% 0m00.38s | 412004 ko | ADTRefinement/BuildADTRefinements/AddCache | 0m00.36s | 412052 ko || +0m00.02s || -48 ko | +5.55% | -0.01% 0m00.38s | 377956 ko | ADTRefinement/GeneralBuildADTTactics | 0m00.36s | 377836 ko || +0m00.02s || 120 ko | +5.55% | +0.03% 0m00.38s | 409872 ko | Common/Ensembles/Cardinal | 0m00.37s | 409704 ko || +0m00.01s || 168 ko | +2.70% | +0.04% 0m00.38s | 426428 ko | Common/Enumerable/ReflectiveForall | 0m00.39s | 426592 ko || -0m00.01s || -164 ko | -2.56% | -0.03% 0m00.38s | 422276 ko | Common/Instances | 0m00.39s | 422308 ko || -0m00.01s || -32 ko | -2.56% | -0.00% 0m00.38s | 420560 ko | Common/Le | 0m00.37s | 420572 ko || +0m00.01s || -12 ko | +2.70% | -0.00% 0m00.38s | 421508 ko | Common/SetoidInstances | 0m00.38s | 421508 ko || +0m00.00s || 0 ko | +0.00% | +0.00% 0m00.38s | 432464 ko | Common/ilist3 | 0m00.41s | 432548 ko || -0m00.02s || -84 ko | -7.31% | -0.01% 0m00.38s | 422140 ko | Parsers/BaseTypesLemmas | 0m00.42s | 422124 ko || -0m00.03s || 16 ko | -9.52% | +0.00% 0m00.38s | 435968 ko | Parsers/Grammars/JSONImpoverishedOriginal | 0m00.35s | 435848 ko || +0m00.03s || 120 ko | +8.57% | +0.02% 0m00.38s | 370724 ko | Parsers/Grammars/StringLiteral | 0m00.29s | 370816 ko || +0m00.09s || -92 ko | +31.03% | -0.02% 0m00.38s | 393068 ko | Parsers/Reflective/ParserReify | 0m00.41s | 393116 ko || -0m00.02s || -48 ko | -7.31% | -0.01% 0m00.38s | 438208 ko | Parsers/Reflective/PartialUnfold | 0m00.36s | 438144 ko || +0m00.02s || 64 ko | +5.55% | +0.01% 0m00.37s | 402816 ko | ADTNotation/BuildComputationalADT | 0m00.34s | 402836 ko || +0m00.02s || -20 ko | +8.82% | -0.00% 0m00.37s | 391368 ko | ADTRefinement/Core | 0m00.31s | 391388 ko || +0m00.06s || -20 ko | +19.35% | -0.00% 0m00.37s | 431708 ko | ADTRefinement/Refinements/HoneRepresentation | 0m00.39s | 431536 ko || -0m00.02s || 172 ko | -5.12% | +0.03% 0m00.37s | 410620 ko | ADTRefinement/Refinements/RefineHideADT | 0m00.36s | 410676 ko || +0m00.01s || -56 ko | +2.77% | -0.01% 0m00.37s | 403708 ko | Common/Enumerable/ReflectiveForallStaged | 0m00.37s | 403600 ko || +0m00.00s || 108 ko | +0.00% | +0.02% 0m00.37s | 394084 ko | Computation/LogicLemmas | 0m00.37s | 394208 ko || +0m00.00s || -124 ko | +0.00% | -0.03% 0m00.37s | 370432 ko | Parsers/BooleanRecognizerFull | 0m00.38s | 370600 ko || -0m00.01s || -168 ko | -2.63% | -0.04% 0m00.37s | 344568 ko | Parsers/Reachable/ParenBalancedHiding/Core | 0m00.39s | 344740 ko || -0m00.02s || -172 ko | -5.12% | -0.04% 0m00.37s | 349160 ko | Parsers/Reflective/Semantics | 0m00.36s | 349068 ko || +0m00.01s || 92 ko | +2.77% | +0.02% 0m00.37s | 415400 ko | Parsers/Reflective/SyntaxEquivalence | 0m00.37s | 415320 ko || +0m00.00s || 80 ko | +0.00% | +0.01% 0m00.37s | 420456 ko | Parsers/StringLike/Core | 0m00.36s | 420372 ko || +0m00.01s || 84 ko | +2.77% | +0.01% 0m00.36s | 388832 ko | ADTNotation/BuildADTReplaceMethods | 0m00.35s | 388764 ko || +0m00.01s || 68 ko | +2.85% | +0.01% 0m00.36s | 356632 ko | ADTRefinement/BuildADTRefinements | 0m00.36s | 356704 ko || +0m00.00s || -72 ko | +0.00% | -0.02% 0m00.36s | 398172 ko | Common/Prod | 0m00.34s | 398180 ko || +0m00.01s || -8 ko | +5.88% | -0.00% 0m00.36s | 422296 ko | Common/SetEq | 0m00.36s | 422336 ko || +0m00.00s || -40 ko | +0.00% | -0.00% 0m00.36s | 431632 ko | Common/i3list2 | 0m00.39s | 431664 ko || -0m00.03s || -32 ko | -7.69% | -0.00% 0m00.36s | 371724 ko | Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretationDefinitionsRelations | 0m00.34s | 371700 ko || +0m00.01s || 24 ko | +5.88% | +0.00% 0m00.36s | 342200 ko | Parsers/ContextFreeGrammar/Precompute | 0m00.34s | 341984 ko || +0m00.01s || 216 ko | +5.88% | +0.06% 0m00.36s | 378688 ko | Parsers/Grammars/ExpressionNumPlusParen | 0m00.35s | 378764 ko || +0m00.01s || -76 ko | +2.85% | -0.02% 0m00.36s | 360808 ko | Parsers/Reachable/ParenBalancedHiding/WellFounded | 0m00.33s | 360684 ko || +0m00.02s || 124 ko | +9.09% | +0.03% 0m00.36s | 409920 ko | Parsers/Reflective/ParserSoundnessOptimized | 0m00.38s | 409820 ko || -0m00.02s || 100 ko | -5.26% | +0.02% 0m00.35s | 356312 ko | ADTNotation/BuildADTSig | 0m00.35s | 356380 ko || +0m00.00s || -68 ko | +0.00% | -0.01% 0m00.35s | 403740 ko | ADTRefinement/BuildADTSetoidMorphisms | 0m00.38s | 403712 ko || -0m00.03s || 28 ko | -7.89% | +0.00% 0m00.35s | 420920 ko | Common/UIP | 0m00.38s | 420904 ko || -0m00.03s || 16 ko | -7.89% | +0.00% 0m00.35s | 409764 ko | Common/i2list2 | 0m00.34s | 409800 ko || +0m00.00s || -36 ko | +2.94% | -0.00% 0m00.35s | 336648 ko | Parsers/ContextFreeGrammar/ReflectiveLemmas | 0m00.33s | 336472 ko || +0m00.01s || 176 ko | +6.06% | +0.05% 0m00.35s | 422236 ko | Parsers/ContextFreeGrammar/SimpleCorrectnessLemmas | 0m00.35s | 422256 ko || +0m00.00s || -20 ko | +0.00% | -0.00% 0m00.35s | 435524 ko | Parsers/Grammars/JSON | 0m00.37s | 435632 ko || -0m00.02s || -108 ko | -5.40% | -0.02% 0m00.35s | 342368 ko | Parsers/ParserInterface | 0m00.36s | 342496 ko || -0m00.01s || -128 ko | -2.77% | -0.03% 0m00.35s | 335588 ko | Parsers/Reachable/All/Reachable | 0m00.34s | 335588 ko || +0m00.00s || 0 ko | +2.94% | +0.00% 0m00.35s | 288028 ko | Parsers/Reflective/Reify | 0m00.33s | 288132 ko || +0m00.01s || -104 ko | +6.06% | -0.03% 0m00.35s | 347768 ko | Parsers/StringLike | 0m00.33s | 347720 ko || +0m00.01s || 48 ko | +6.06% | +0.01% 0m00.34s | 376084 ko | ADT/ADTSig | 0m00.33s | 376128 ko || +0m00.01s || -44 ko | +3.03% | -0.01% 0m00.34s | 377556 ko | ADTRefinement/Refinements/SimplifyRep | 0m00.35s | 377536 ko || -0m00.00s || 20 ko | -2.85% | +0.00% 0m00.34s | 370288 ko | Common/StringBound | 0m00.30s | 370504 ko || +0m00.04s || -216 ko | +13.33% | -0.05% 0m00.34s | 401184 ko | Common/ilist3_pair | 0m00.36s | 401196 ko || -0m00.01s || -12 ko | -5.55% | -0.00% 0m00.34s | 338760 ko | Computation | 0m00.33s | 338824 ko || +0m00.01s || -64 ko | +3.03% | -0.01% 0m00.34s | 357572 ko | Computation/FueledFix | 0m00.34s | 357476 ko || +0m00.00s || 96 ko | +0.00% | +0.02% 0m00.34s | 356200 ko | Parsers/ContextFreeGrammar/Fix/Inject | 0m00.31s | 355996 ko || +0m00.03s || 204 ko | +9.67% | +0.05% 0m00.34s | 339372 ko | Parsers/ContextFreeGrammar/PreNotations | 0m00.38s | 339312 ko || -0m00.03s || 60 ko | -10.52% | +0.01% 0m00.34s | 340264 ko | Parsers/ContextFreeGrammar/PreNotationsLemmas | 0m00.32s | 340008 ko || +0m00.02s || 256 ko | +6.25% | +0.07% 0m00.34s | 341532 ko | Parsers/ContextFreeGrammar/TransferProperties | 0m00.36s | 341528 ko || -0m00.01s || 4 ko | -5.55% | +0.00% 0m00.34s | 355936 ko | Parsers/Grammars/FlatComments | 0m00.33s | 355912 ko || +0m00.01s || 24 ko | +3.03% | +0.00% 0m00.34s | 335124 ko | Parsers/Reachable/All/ReachableWellFounded | 0m00.31s | 335108 ko || +0m00.03s || 16 ko | +9.67% | +0.00% 0m00.34s | 349012 ko | Parsers/Reflective/ParserSyntaxEquivalence | 0m00.33s | 348920 ko || +0m00.01s || 92 ko | +3.03% | +0.02% 0m00.34s | 352716 ko | Parsers/Reflective/SemanticsOptimized | 0m00.34s | 352828 ko || +0m00.00s || -112 ko | +0.00% | -0.03% 0m00.33s | 376672 ko | ADT/ADTHide | 0m00.36s | 376564 ko || -0m00.02s || 108 ko | -8.33% | +0.02% 0m00.33s | 348044 ko | ADTRefinement | 0m00.33s | 348276 ko || +0m00.00s || -232 ko | +0.00% | -0.06% 0m00.33s | 390176 ko | ADTRefinement/BuildADTRefinements/SimplifyRep | 0m00.35s | 390024 ko || -0m00.01s || 152 ko | -5.71% | +0.03% 0m00.33s | 340308 ko | Parsers/ActionEvaluator | 0m00.32s | 340200 ko || +0m00.01s || 108 ko | +3.12% | +0.03% 0m00.33s | 360364 ko | Parsers/BooleanRecognizer | 0m00.32s | 360548 ko || +0m00.01s || -184 ko | +3.12% | -0.05% 0m00.33s | 339804 ko | Parsers/ContextFreeGrammar/Notations | 0m00.34s | 339764 ko || -0m00.01s || 40 ko | -2.94% | +0.01% 0m00.33s | 343948 ko | Parsers/ExtrOcamlPrimitives | 0m00.27s | 344108 ko || +0m00.06s || -160 ko | +22.22% | -0.04% 0m00.33s | 338776 ko | Parsers/Grammars/Trivial | 0m00.32s | 338844 ko || +0m00.01s || -68 ko | +3.12% | -0.02% 0m00.32s | 343904 ko | ADT | 0m00.34s | 343736 ko || -0m00.02s || 168 ko | -5.88% | +0.04% 0m00.32s | 348308 ko | ADTNotation | 0m00.31s | 348208 ko || +0m00.01s || 100 ko | +3.22% | +0.02% 0m00.32s | 384924 ko | ADTRefinement/Refinements/DelegateMethods | 0m00.31s | 385112 ko || +0m00.01s || -188 ko | +3.22% | -0.04% 0m00.32s | 383176 ko | Common/Ensembles/Equivalence | 0m00.32s | 383252 ko || +0m00.00s || -76 ko | +0.00% | -0.01% 0m00.32s | 300328 ko | Common/EnumType | 0m00.34s | 300152 ko || -0m00.02s || 176 ko | -5.88% | +0.05% 0m00.32s | 388204 ko | Common/OptionFacts | 0m00.31s | 388184 ko || +0m00.01s || 20 ko | +3.22% | +0.00% 0m00.32s | 378416 ko | Parsers/CorrectnessBaseTypes | 0m00.32s | 378560 ko || +0m00.00s || -144 ko | +0.00% | -0.03% 0m00.32s | 336160 ko | Parsers/Reachable/OnlyFirst/Reachable | 0m00.29s | 336024 ko || +0m00.03s || 136 ko | +10.34% | +0.04% 0m00.32s | 335804 ko | Parsers/Reachable/OnlyFirst/ReachableWellFounded | 0m00.32s | 335680 ko || +0m00.00s || 124 ko | +0.00% | +0.03% 0m00.32s | 357152 ko | Parsers/Reachable/ParenBalanced/WellFounded | 0m00.34s | 357200 ko || -0m00.02s || -48 ko | -5.88% | -0.01% 0m00.32s | 345472 ko | Parsers/Reflective/ParserPartialUnfold | 0m00.34s | 345384 ko || -0m00.02s || 88 ko | -5.88% | +0.02% 0m00.32s | 330788 ko | Parsers/Specification | 0m00.29s | 330832 ko || +0m00.03s || -44 ko | +10.34% | -0.01% 0m00.31s | 332156 ko | Common/Tactics/CacheStringConstant | 0m00.32s | 332116 ko || -0m00.01s || 40 ko | -3.12% | +0.01% 0m00.31s | 359312 ko | Computation/Core | 0m00.34s | 359144 ko || -0m00.03s || 168 ko | -8.82% | +0.04% 0m00.31s | 335500 ko | Computation/SetoidEqMorphisms | 0m00.31s | 335668 ko || +0m00.00s || -168 ko | +0.00% | -0.05% 0m00.31s | 382404 ko | Parsers/GenericRecognizer | 0m00.33s | 382328 ko || -0m00.02s || 76 ko | -6.06% | +0.01% 0m00.31s | 365352 ko | Parsers/Grammars/JSComment | 0m00.32s | 365120 ko || -0m00.01s || 232 ko | -3.12% | +0.06% 0m00.31s | 280744 ko | Parsers/Reflective/Syntactify | 0m00.32s | 280600 ko || -0m00.01s || 144 ko | -3.12% | +0.05% 0m00.30s | 376640 ko | ADT/Core | 0m00.31s | 376756 ko || -0m00.01s || -116 ko | -3.22% | -0.03% 0m00.30s | 347664 ko | ADTRefinement/Refinements | 0m00.33s | 347608 ko || -0m00.03s || 56 ko | -9.09% | +0.01% 0m00.30s | 354268 ko | Common/Ensembles | 0m00.31s | 354392 ko || -0m00.01s || -124 ko | -3.22% | -0.03% 0m00.30s | 360084 ko | Common/Ensembles/Tactics | 0m00.30s | 360100 ko || +0m00.00s || -16 ko | +0.00% | -0.00% 0m00.30s | 386000 ko | Common/Monad | 0m00.31s | 385940 ko || -0m00.01s || 60 ko | -3.22% | +0.01% 0m00.30s | 390140 ko | Common/Telescope/Instances | 0m00.31s | 390168 ko || -0m00.01s || -28 ko | -3.22% | -0.00% 0m00.30s | 360152 ko | Computation/Refinements/Tactics | 0m00.31s | 359928 ko || -0m00.01s || 224 ko | -3.22% | +0.06% 0m00.30s | 349584 ko | Parsers/Grammars/ABStar | 0m00.32s | 349792 ko || -0m00.02s || -208 ko | -6.25% | -0.05% 0m00.30s | 350788 ko | Parsers/Grammars/ExpressionNumPlus | 0m00.33s | 350840 ko || -0m00.03s || -52 ko | -9.09% | -0.01% 0m00.30s | 349996 ko | Parsers/Grammars/ExpressionParen | 0m00.34s | 349932 ko || -0m00.04s || 64 ko | -11.76% | +0.01% 0m00.30s | 334676 ko | Parsers/Reachable/MaybeEmpty/WellFounded | 0m00.31s | 334680 ko || -0m00.01s || -4 ko | -3.22% | -0.00% 0m00.30s | 336116 ko | Parsers/Reachable/OnlyLast/Reachable | 0m00.35s | 336004 ko || -0m00.04s || 112 ko | -14.28% | +0.03% 0m00.30s | 335760 ko | Parsers/Reachable/OnlyLast/ReachableWellFounded | 0m00.34s | 335568 ko || -0m00.04s || 192 ko | -11.76% | +0.05% 0m00.30s | 342392 ko | Parsers/Reflective/ParserSyntax | 0m00.28s | 342456 ko || +0m00.01s || -64 ko | +7.14% | -0.01% 0m00.29s | 383724 ko | Parsers/GenericBoolCorrectnessBaseTypes | 0m00.27s | 383856 ko || +0m00.01s || -132 ko | +7.40% | -0.03% 0m00.29s | 373960 ko | Parsers/Grammars/EvalGrammarTactics | 0m00.32s | 373876 ko || -0m00.03s || 84 ko | -9.37% | +0.02% 0m00.29s | 335612 ko | Parsers/Reachable/MaybeEmpty/Core | 0m00.32s | 335452 ko || -0m00.03s || 160 ko | -9.37% | +0.04% 0m00.29s | 377920 ko | Parsers/SimpleRecognizer | 0m00.34s | 377984 ko || -0m00.05s || -64 ko | -14.70% | -0.01% 0m00.28s | 253464 ko | Common/Coq__8_4__8_5__Compat | 0m00.26s | 253600 ko || +0m00.02s || -136 ko | +7.69% | -0.05% 0m00.28s | 386844 ko | Common/LogicMorphisms | 0m00.28s | 386828 ko || +0m00.00s || 16 ko | +0.00% | +0.00% 0m00.27s | 328200 ko | Parsers/MinimalParse | 0m00.22s | 328336 ko || +0m00.05s || -136 ko | +22.72% | -0.04% 0m00.26s | 298860 ko | Common/Match | 0m00.25s | 298904 ko || +0m00.01s || -44 ko | +4.00% | -0.01% 0m00.26s | 320872 ko | Parsers/ContextFreeGrammar/Transfer | 0m00.22s | 321044 ko || +0m00.04s || -172 ko | +18.18% | -0.05% 0m00.26s | 269744 ko | Parsers/Grammars/JavaScriptExpression | 0m00.22s | 269740 ko || +0m00.04s || 4 ko | +18.18% | +0.00% 0m00.26s | 269856 ko | Parsers/Grammars/JavaScriptStatementsWithoutAssignmentExpression | 0m00.20s | 269828 ko || +0m00.06s || 28 ko | +30.00% | +0.01% 0m00.25s | 279628 ko | Common/VectorFacts | 0m00.23s | 279568 ko || +0m00.01s || 60 ko | +8.69% | +0.02% 0m00.25s | 314432 ko | Parsers/Reachable/OnlyFirst/MinimalReachable | 0m00.23s | 314420 ko || +0m00.01s || 12 ko | +8.69% | +0.00% 0m00.24s | 385360 ko | Common/SetoidClassInstances | 0m00.27s | 385404 ko || -0m00.03s || -44 ko | -11.11% | -0.01% 0m00.24s | 296700 ko | Common/StringOperations | 0m00.24s | 296800 ko || +0m00.00s || -100 ko | +0.00% | -0.03% 0m00.24s | 272176 ko | Common/Tactics/DestructHyps | 0m00.22s | 272076 ko || +0m00.01s || 100 ko | +9.09% | +0.03% 0m00.24s | 269704 ko | Common/Tactics/FreeIn | 0m00.21s | 269832 ko || +0m00.03s || -128 ko | +14.28% | -0.04% 0m00.24s | 269840 ko | Common/Tactics/Head | 0m00.22s | 270032 ko || +0m00.01s || -192 ko | +9.09% | -0.07% 0m00.24s | 321932 ko | Parsers/ContextFreeGrammar/Core | 0m00.24s | 321824 ko || +0m00.00s || 108 ko | +0.00% | +0.03% 0m00.24s | 299936 ko | Parsers/GenericBaseTypes | 0m00.22s | 300092 ko || +0m00.01s || -156 ko | +9.09% | -0.05% 0m00.24s | 312944 ko | Parsers/Reachable/All/MinimalReachable | 0m00.21s | 312912 ko || +0m00.03s || 32 ko | +14.28% | +0.01% 0m00.24s | 314472 ko | Parsers/Reachable/OnlyLast/MinimalReachable | 0m00.21s | 314448 ko || +0m00.03s || 24 ko | +14.28% | +0.00% 0m00.24s | 269620 ko | Parsers/Refinement/DisjointLemmasEarlyDeclarations | 0m00.21s | 269788 ko || +0m00.03s || -168 ko | +14.28% | -0.06% 0m00.24s | 311400 ko | Parsers/WellFoundedParse | 0m00.24s | 311488 ko || +0m00.00s || -88 ko | +0.00% | -0.02% 0m00.23s | 271352 ko | Common/Notations | 0m00.19s | 271456 ko || +0m00.04s || -104 ko | +21.05% | -0.03% 0m00.23s | 377220 ko | Common/PointedProp | 0m00.30s | 377288 ko || -0m00.06s || -68 ko | -23.33% | -0.01% 0m00.23s | 270968 ko | Common/Tactics/SpecializeBy | 0m00.23s | 270904 ko || +0m00.00s || 64 ko | +0.00% | +0.02% 0m00.23s | 270800 ko | Common/Tactics/SplitInContext | 0m00.21s | 270920 ko || +0m00.02s || -120 ko | +9.52% | -0.04% 0m00.23s | 300632 ko | Common/Telescope/Core | 0m00.23s | 300460 ko || +0m00.00s || 172 ko | +0.00% | +0.05% 0m00.23s | 269840 ko | Computation/Notations | 0m00.22s | 269860 ko || +0m00.01s || -20 ko | +4.54% | -0.00% 0m00.23s | 269244 ko | Parsers/BooleanRecognizerMin | 0m00.20s | 269228 ko || +0m00.03s || 16 ko | +15.00% | +0.00% 0m00.23s | 323888 ko | Parsers/ContextFreeGrammar/SimpleCorrectness | 0m00.23s | 323688 ko || +0m00.00s || 200 ko | +0.00% | +0.06% 0m00.22s | 270964 ko | Common/Ensembles/Notations | 0m00.22s | 270880 ko || +0m00.00s || 84 ko | +0.00% | +0.03% 0m00.22s | 274588 ko | Common/Tactics/BreakMatch | 0m00.24s | 274364 ko || -0m00.01s || 224 ko | -8.33% | +0.08% 0m00.22s | 269972 ko | Common/Tactics/Combinators | 0m00.24s | 270068 ko || -0m00.01s || -96 ko | -8.33% | -0.03% 0m00.22s | 272376 ko | Common/Tactics/DestructHead | 0m00.23s | 272604 ko || -0m00.01s || -228 ko | -4.34% | -0.08% 0m00.22s | 270060 ko | Common/Tactics/FoldIsTrue | 0m00.22s | 269952 ko || +0m00.00s || 108 ko | +0.00% | +0.04% 0m00.22s | 269860 ko | Common/Tactics/GetGoal | 0m00.23s | 269556 ko || -0m00.01s || 304 ko | -4.34% | +0.11% 0m00.22s | 269600 ko | Common/Tactics/IsClosed | 0m00.22s | 269876 ko || +0m00.00s || -276 ko | +0.00% | -0.10% 0m00.22s | 270112 ko | Common/Tactics/PrintContext | 0m00.24s | 270088 ko || -0m00.01s || 24 ko | -8.33% | +0.00% 0m00.22s | 338856 ko | Parsers/BaseTypes | 0m00.24s | 338624 ko || -0m00.01s || 232 ko | -8.33% | +0.06% 0m00.22s | 300880 ko | Parsers/ContextFreeGrammar/Valid | 0m00.22s | 300944 ko || +0m00.00s || -64 ko | +0.00% | -0.02% 0m00.22s | 310980 ko | Parsers/Reachable/MaybeEmpty/Minimal | 0m00.23s | 311136 ko || -0m00.01s || -156 ko | -4.34% | -0.05% 0m00.21s | 285428 ko | Common/LetIn | 0m00.23s | 285376 ko || -0m00.02s || 52 ko | -8.69% | +0.01% 0m00.21s | 270332 ko | Common/Tactics/DestructSig | 0m00.24s | 270356 ko || -0m00.03s || -24 ko | -12.50% | -0.00% 0m00.21s | 269788 ko | Parsers/Grammars/JavaScriptWithoutStatements | 0m00.24s | 269836 ko || -0m00.03s || -48 ko | -12.50% | -0.01% 0m00.21s | 270096 ko | Parsers/Refinement/DisjointRulesCommon | 0m00.22s | 269964 ko || -0m00.01s || 132 ko | -4.54% | +0.04% 0m00.20s | 273212 ko | Common/Tactics/SetoidSubst | 0m00.22s | 273284 ko || -0m00.01s || -72 ko | -9.09% | -0.02% 0m00.19s | 269932 ko | Common/ReservedNotations | 0m00.25s | 269740 ko || -0m00.06s || 192 ko | -24.00% | +0.07% 0m00.04s | 60228 ko | Common/Tactics/HintDbExtra | 0m00.05s | 60308 ko || -0m00.01s || -80 ko | -20.00% | -0.13% 0m00.04s | 60616 ko | Common/Tactics/TransparentAbstract | 0m00.04s | 60508 ko || +0m00.00s || 108 ko | +0.00% | +0.17% 0m00.03s | 15744 ko | Common/Tactics/hint_db_extra_plugin | 0m00.02s | 15672 ko || +0m00.00s || 72 ko | +49.99% | +0.45% 0m00.03s | 15740 ko | Common/Tactics/transparent_abstract_plugin | 0m00.03s | 15736 ko || +0m00.00s || 4 ko | +0.00% | +0.02% 0m00.02s | 23320 ko | Common/Tactics/hint_db_extra_tactics | 0m00.02s | 23376 ko || +0m00.00s || -56 ko | +0.00% | -0.23% 0m00.02s | 22036 ko | Common/Tactics/transparent_abstract_tactics | 0m00.01s | 22016 ko || +0m00.01s || 20 ko | +100.00% | +0.09% ```

Diff between 47088d083967e55b6cd1ec12fceb06892dfb33bf (after) and 21bc38e31e498465854e57eb8bc791523f100c4e (before)

``` 47088d0 | Peak Mem | File Name | 21bc38e | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ 7m19.19s | 863012 ko | Total Time / Peak Mem | 7m33.37s | 871544 ko || -0m14.17s || -8532 ko | -3.12% | -0.97% ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ 0m17.92s | 587684 ko | Parsers/Refinement/PossibleTerminalsSets | 0m20.75s | 597996 ko || -0m02.82s || -10312 ko | -13.63% | -1.72% 0m05.04s | 510712 ko | Parsers/ContextFreeGrammar/Fix/Fix | 0m07.52s | 512184 ko || -0m02.47s || -1472 ko | -32.97% | -0.28% 0m00.99s | 498564 ko | Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretation | 0m02.67s | 497136 ko || -0m01.68s || 1428 ko | -62.92% | +0.28% 0m22.93s | 737196 ko | Parsers/ParserFromParserADT | 0m22.95s | 739528 ko || -0m00.01s || -2332 ko | -0.08% | -0.31% 0m21.76s | 690716 ko | Parsers/GenericRecognizerMin | 0m21.84s | 694412 ko || -0m00.07s || -3696 ko | -0.36% | -0.53% 0m19.89s | 863012 ko | Parsers/BooleanRecognizerOptimized | 0m19.71s | 871544 ko || +0m00.17s || -8532 ko | +0.91% | -0.97% 0m15.95s | 800432 ko | Parsers/GenericRecognizerOptimized | 0m16.05s | 800008 ko || -0m00.10s || 424 ko | -0.62% | +0.05% 0m15.82s | 812884 ko | Parsers/BooleanRecognizerOptimizedReflectiveCorrectness | 0m16.44s | 816344 ko || -0m00.62s || -3460 ko | -3.77% | -0.42% 0m14.27s | 569248 ko | Parsers/SplitterFromParserADT | 0m14.26s | 571240 ko || +0m00.00s || -1992 ko | +0.07% | -0.34% 0m10.67s | 477936 ko | Common/FMapExtensions | 0m10.91s | 479988 ko || -0m00.24s || -2052 ko | -2.19% | -0.42% 0m10.26s | 796564 ko | Parsers/Reflective/LogicalRelations | 0m10.25s | 796260 ko || +0m00.00s || 304 ko | +0.09% | +0.03% 0m10.10s | 465724 ko | Parsers/Refinement/BinOpBrackets/MakeBinOpTable | 0m10.71s | 466752 ko || -0m00.61s || -1028 ko | -5.69% | -0.22% 0m09.50s | 639084 ko | Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflective | 0m09.06s | 636068 ko || +0m00.43s || 3016 ko | +4.85% | +0.47% 0m06.14s | 470860 ko | Common/List/ListFacts | 0m06.09s | 469896 ko || +0m00.04s || 964 ko | +0.82% | +0.20% 0m05.41s | 545880 ko | Parsers/StringLike/LastChar | 0m05.55s | 546748 ko || -0m00.13s || -868 ko | -2.52% | -0.15% 0m04.61s | 456256 ko | Parsers/Grammars/Tests | 0m04.36s | 452608 ko || +0m00.25s || 3648 ko | +5.73% | +0.80% 0m04.59s | 442636 ko | Parsers/StringLike/FirstCharSuchThat | 0m04.46s | 441544 ko || +0m00.12s || 1092 ko | +2.91% | +0.24% 0m04.58s | 570052 ko | Parsers/Refinement/DisjointRulesRev | 0m04.57s | 569940 ko || +0m00.00s || 112 ko | +0.21% | +0.01% 0m04.49s | 500508 ko | Parsers/MinimalParseOfParse | 0m04.80s | 506948 ko || -0m00.30s || -6440 ko | -6.45% | -1.27% 0m04.36s | 488840 ko | Parsers/Grammars/JSONTests | 0m04.29s | 488724 ko || +0m00.07s || 116 ko | +1.63% | +0.02% 0m04.33s | 509148 ko | Parsers/StringLike/OcamlString | 0m04.28s | 509420 ko || +0m00.04s || -272 ko | +1.16% | -0.05% 0m04.18s | 445580 ko | Parsers/StringLike/Properties | 0m04.73s | 445264 ko || -0m00.55s || 316 ko | -11.62% | +0.07% 0m03.82s | 559092 ko | Parsers/Refinement/IndexedAndAtMostOneNonTerminalReflectiveOpt | 0m03.97s | 558136 ko || -0m00.15s || 956 ko | -3.77% | +0.17% 0m03.64s | 460556 ko | Parsers/ContextFreeGrammar/Fix/ProdAbstractInterpretationDefinitions | 0m03.64s | 460452 ko || +0m00.00s || 104 ko | +0.00% | +0.02% 0m03.64s | 579428 ko | Parsers/Refinement/DisjointRules | 0m03.52s | 580480 ko || +0m00.12s || -1052 ko | +3.40% | -0.18% 0m03.53s | 441856 ko | Common/Ensembles/IndexedEnsembles | 0m03.53s | 440704 ko || +0m00.00s || 1152 ko | +0.00% | +0.26% 0m03.46s | 478652 ko | Common/FMapExtensions/LiftRelationInstances | 0m03.47s | 476932 ko || -0m00.01s || 1720 ko | -0.28% | +0.36% 0m03.34s | 451512 ko | Parsers/AbstractInterpretation/NonTerminalMap | 0m03.87s | 451248 ko || -0m00.53s || 264 ko | -13.69% | +0.05% 0m03.25s | 505872 ko | Parsers/BooleanRecognizerOptimizedReflective | 0m03.30s | 506048 ko || -0m00.04s || -176 ko | -1.51% | -0.03% 0m03.16s | 454036 ko | Parsers/Grammars/JavaScript | 0m03.27s | 454148 ko || -0m00.10s || -112 ko | -3.36% | -0.02% 0m03.01s | 500024 ko | Parsers/ContextFreeGrammar/Fix/FixRelated | 0m03.79s | 499448 ko || -0m00.78s || 576 ko | -20.58% | +0.11% 0m02.96s | 467580 ko | Parsers/SimpleRecognizerCorrect | 0m02.99s | 467212 ko || -0m00.03s || 368 ko | -1.00% | +0.07% 0m02.92s | 440588 ko | Parsers/Refinement/BinOpBrackets/ParenBalancedLemmas | 0m03.05s | 441072 ko || -0m00.12s || -484 ko | -4.26% | -0.10% 0m02.87s | 592456 ko | Parsers/Refinement/SharpenedJSComment | 0m02.84s | 592268 ko || +0m00.03s || 188 ko | +1.05% | +0.03% 0m02.83s | 496708 ko | Parsers/Refinement/EmptyLemmas | 0m02.72s | 496812 ko || +0m00.10s || -104 ko | +4.04% | -0.02% 0m02.76s | 452916 ko | Parsers/Refinement/FinishingLemma | 0m02.77s | 452928 ko || -0m00.01s || -12 ko | -0.36% | -0.00% 0m02.62s | 463612 ko | Common/Wf2 | 0m02.81s | 462268 ko || -0m00.18s || 1344 ko | -6.76% | +0.29% 0m02.51s | 630988 ko | Parsers/Refinement/SharpenedExpressionPlus | 0m02.49s | 631064 ko || +0m00.01s || -76 ko | +0.80% | -0.01% 0m02.41s | 445912 ko | Parsers/Refinement/BinOpBrackets/ParenBalancedGrammar | 0m02.41s | 445216 ko || +0m00.00s || 696 ko | +0.00% | +0.15% 0m02.36s | 585180 ko | Parsers/Refinement/BinOpBrackets/BinOpRules | 0m02.40s | 585048 ko || -0m00.04s || 132 ko | -1.66% | +0.02% 0m02.35s | 634932 ko | Parsers/Refinement/SharpenedExpressionPlusParen | 0m02.35s | 634812 ko || +0m00.00s || 120 ko | +0.00% | +0.01% 0m02.32s | 446152 ko | Parsers/GenericRecognizerExt | 0m02.81s | 445700 ko || -0m00.49s || 452 ko | -17.43% | +0.10% 0m02.29s | 497232 ko | Parsers/Refinement/FixedLengthLemmas | 0m02.55s | 496220 ko || -0m00.25s || 1012 ko | -10.19% | +0.20% 0m02.29s | 440708 ko | Parsers/StringLike/ForallChars | 0m02.25s | 438288 ko || +0m00.04s || 2420 ko | +1.77% | +0.55% 0m02.08s | 496352 ko | Common/FMapExtensions/Wf | 0m02.66s | 492196 ko || -0m00.58s || 4156 ko | -21.80% | +0.84% 0m02.03s | 497368 ko | Parsers/ContextFreeGrammar/Fix/Correct | 0m02.10s | 496696 ko || -0m00.07s || 672 ko | -3.33% | +0.13% 0m02.02s | 439296 ko | Parsers/Splitters/RDPList | 0m02.05s | 439152 ko || -0m00.02s || 144 ko | -1.46% | +0.03% 0m01.99s | 445224 ko | Parsers/ContextFreeGrammar/Fix/Prod | 0m02.34s | 444684 ko || -0m00.34s || 540 ko | -14.95% | +0.12% 0m01.95s | 582700 ko | Parsers/Refinement/SharpenedStringLiteral | 0m01.95s | 582120 ko || +0m00.00s || 580 ko | +0.00% | +0.09% 0m01.85s | 443044 ko | Computation/Refinements/General | 0m01.90s | 443100 ko || -0m00.04s || -56 ko | -2.63% | -0.01% 0m01.84s | 445844 ko | Parsers/Refinement/BinOpBrackets/ParenBalanced | 0m02.12s | 444676 ko || -0m00.28s || 1168 ko | -13.20% | +0.26% 0m01.83s | 431836 ko | Common/BoundedLookup | 0m01.74s | 431844 ko || +0m00.09s || -8 ko | +5.17% | -0.00% 0m01.77s | 440916 ko | Parsers/StringLike/LastCharSuchThat | 0m01.83s | 440852 ko || -0m00.06s || 64 ko | -3.27% | +0.01% 0m01.68s | 627692 ko | Parsers/Refinement/SharpenedExpressionPlusParenParseTree | 0m01.61s | 627588 ko || +0m00.06s || 104 ko | +4.34% | +0.01% 0m01.67s | 432660 ko | Common/Frame | 0m01.74s | 432468 ko || -0m00.07s || 192 ko | -4.02% | +0.04% 0m01.66s | 438152 ko | Common/List/ListMorphisms | 0m01.90s | 437984 ko || -0m00.24s || 168 ko | -12.63% | +0.03% 0m01.65s | 437296 ko | Common/Ensembles/EnsembleListEquivalence | 0m01.66s | 437100 ko || -0m00.01s || 196 ko | -0.60% | +0.04% 0m01.60s | 448696 ko | Parsers/GenericRecognizerBoolEquality | 0m01.59s | 448500 ko || +0m00.01s || 196 ko | +0.62% | +0.04% 0m01.57s | 450912 ko | Parsers/RecognizerPreOptimized | 0m01.64s | 450956 ko || -0m00.06s || -44 ko | -4.26% | -0.00% 0m01.55s | 443284 ko | Common/StringFacts | 0m01.58s | 443468 ko || -0m00.03s || -184 ko | -1.89% | -0.04% 0m01.55s | 441548 ko | Common/Wf1 | 0m01.70s | 441800 ko || -0m00.14s || -252 ko | -8.82% | -0.05% 0m01.54s | 577684 ko | Parsers/Refinement/SharpenedABStar | 0m01.55s | 573544 ko || -0m00.01s || 4140 ko | -0.64% | +0.72% 0m01.51s | 438064 ko | Common | 0m01.55s | 437984 ko || -0m00.04s || 80 ko | -2.58% | +0.01% 0m01.44s | 455896 ko | Parsers/Reachable/ParenBalancedHiding/MinimalOfCore | 0m01.45s | 455968 ko || -0m00.01s || -72 ko | -0.68% | -0.01% 0m01.44s | 464224 ko | Parsers/Reflective/SyntaxEquality | 0m01.40s | 464092 ko || +0m00.04s || 132 ko | +2.85% | +0.02% 0m01.43s | 441196 ko | Parsers/StringLike/FirstChar | 0m01.46s | 441584 ko || -0m00.03s || -388 ko | -2.05% | -0.08% 0m01.33s | 453284 ko | ADTRefinement/FixedPoint | 0m01.99s | 452420 ko || -0m00.65s || 864 ko | -33.16% | +0.19% 0m01.31s | 438764 ko | Parsers/Reflective/SyntaxEquivalenceReflective | 0m01.36s | 438740 ko || -0m00.05s || 24 ko | -3.67% | +0.00% 0m01.29s | 570880 ko | Parsers/Refinement/SharpenedExpressionParen | 0m01.39s | 570852 ko || -0m00.09s || 28 ko | -7.19% | +0.00% 0m01.26s | 448388 ko | Parsers/Grammars/JavaScriptAssignmentExpression | 0m01.26s | 448304 ko || +0m00.00s || 84 ko | +0.00% | +0.01% 0m01.25s | 442564 ko | Common/List/PermutationFacts | 0m01.23s | 442552 ko || +0m00.02s || 12 ko | +1.62% | +0.00% 0m01.23s | 451692 ko | Parsers/Reachable/ParenBalanced/MinimalOfCore | 0m01.14s | 451776 ko || +0m00.09s || -84 ko | +7.89% | -0.01% 0m01.19s | 443052 ko | Computation/FixComp | 0m01.15s | 443196 ko || +0m00.04s || -144 ko | +3.47% | -0.03% 0m01.18s | 430268 ko | Common/DecideableEnsembles | 0m01.16s | 430236 ko || +0m00.02s || 32 ko | +1.72% | +0.00% 0m01.08s | 564760 ko | Parsers/Refinement/DisjointLemmas | 0m01.08s | 564728 ko || +0m00.00s || 32 ko | +0.00% | +0.00% 0m01.06s | 436608 ko | Common/Enumerable/ReflectiveForallAggregate | 0m01.08s | 436552 ko || -0m00.02s || 56 ko | -1.85% | +0.01% 0m01.06s | 454996 ko | Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretationDefinitions | 0m01.01s | 454664 ko || +0m00.05s || 332 ko | +4.95% | +0.07% 0m01.06s | 469388 ko | Parsers/ParserImplementation | 0m00.97s | 469388 ko || +0m00.09s || 0 ko | +9.27% | +0.00% 0m01.06s | 459336 ko | Parsers/Splitters/BruteForce | 0m01.09s | 456640 ko || -0m00.03s || 2696 ko | -2.75% | +0.59% 0m01.03s | 451588 ko | Common/MSetBoundedLattice | 0m00.98s | 452280 ko || +0m00.05s || -692 ko | +5.10% | -0.15% 0m01.02s | 437632 ko | Common/NatFacts | 0m01.04s | 437724 ko || -0m00.02s || -92 ko | -1.92% | -0.02% 0m01.00s | 436640 ko | Common/SetEqProperties | 0m01.01s | 436408 ko || -0m00.01s || 232 ko | -0.99% | +0.05% 0m01.00s | 448748 ko | Computation/Refinements/Iterate_Decide_Comp | 0m01.00s | 448648 ko || +0m00.00s || 100 ko | +0.00% | +0.02% 0m00.99s | 443136 ko | Common/MSetExtensions | 0m00.99s | 443164 ko || +0m00.00s || -28 ko | +0.00% | -0.00% 0m00.96s | 437948 ko | Parsers/StringLike/String | 0m00.98s | 437772 ko || -0m00.02s || 176 ko | -2.04% | +0.04% 0m00.95s | 431336 ko | Common/Ensembles/CombinatorLaws | 0m00.96s | 431296 ko || -0m00.01s || 40 ko | -1.04% | +0.00% 0m00.93s | 431664 ko | Computation/SetoidMorphisms | 0m00.93s | 431732 ko || +0m00.00s || -68 ko | +0.00% | -0.01% 0m00.92s | 486064 ko | Parsers/ContextFreeGrammar/Fix/AsciiLattice | 0m01.10s | 486808 ko || -0m00.18s || -744 ko | -16.36% | -0.15% 0m00.90s | 450952 ko | Parsers/Reachable/ParenBalanced/OfParse | 0m00.92s | 450852 ko || -0m00.02s || 100 ko | -2.17% | +0.02% 0m00.89s | 435984 ko | ADTRefinement/SetoidMorphisms | 0m00.83s | 436056 ko || +0m00.06s || -72 ko | +7.22% | -0.01% 0m00.89s | 433196 ko | Common/Equality | 0m00.95s | 433128 ko || -0m00.05s || 68 ko | -6.31% | +0.01% 0m00.89s | 540280 ko | Parsers/ContextFreeGrammar/ExplorationUtil | 0m00.91s | 540424 ko || -0m00.02s || -144 ko | -2.19% | -0.02% 0m00.84s | 435256 ko | Computation/IfDec | 0m00.94s | 435268 ko || -0m00.09s || -12 ko | -10.63% | -0.00% 0m00.83s | 444104 ko | Parsers/ContextFreeGrammar/Fix/Properties | 0m00.99s | 444244 ko || -0m00.16s || -140 ko | -16.16% | -0.03% 0m00.81s | 508224 ko | Parsers/AbstractInterpretation/NonTerminalMapWf | 0m00.84s | 508136 ko || -0m00.02s || 88 ko | -3.57% | +0.01% 0m00.81s | 572444 ko | Parsers/Refinement/Tactics | 0m00.84s | 572392 ko || -0m00.02s || 52 ko | -3.57% | +0.00% 0m00.78s | 438380 ko | Common/Enumerable | 0m00.82s | 438544 ko || -0m00.03s || -164 ko | -4.87% | -0.03% 0m00.78s | 567008 ko | Parsers/Refinement/SharpenedABStarParseTree | 0m00.77s | 566944 ko || +0m00.01s || 64 ko | +1.29% | +0.01% 0m00.77s | 428864 ko | Computation/Decidable | 0m00.75s | 428740 ko || +0m00.02s || 124 ko | +2.66% | +0.02% 0m00.76s | 564260 ko | Parsers/Refinement/ExtractSharpenedABStar | 0m00.79s | 564200 ko || -0m00.03s || 60 ko | -3.79% | +0.01% 0m00.75s | 435212 ko | Common/IterateBoundedIndex | 0m00.71s | 435096 ko || +0m00.04s || 116 ko | +5.63% | +0.02% 0m00.73s | 443800 ko | Computation/ListComputations | 0m00.71s | 443596 ko || +0m00.02s || 204 ko | +2.81% | +0.04% 0m00.71s | 442476 ko | ADTRefinement/BuildADTRefinements/HoneRepresentation | 0m00.83s | 442364 ko || -0m00.12s || 112 ko | -14.45% | +0.02% 0m00.70s | 437684 ko | Parsers/Reachable/MaybeEmpty/MinimalOfCore | 0m00.69s | 437556 ko || +0m00.01s || 128 ko | +1.44% | +0.02% 0m00.69s | 437204 ko | Common/List/UpperBound | 0m00.68s | 437324 ko || +0m00.00s || -120 ko | +1.47% | -0.02% 0m00.69s | 566252 ko | Parsers/ExtrOcamlParsers | 0m00.69s | 566256 ko || +0m00.00s || -4 ko | +0.00% | -0.00% 0m00.68s | 438544 ko | Parsers/Reachable/OnlyLast/MinimalReachableOfReachable | 0m00.69s | 438716 ko || -0m00.00s || -172 ko | -1.44% | -0.03% 0m00.66s | 432428 ko | Computation/FoldComp | 0m00.67s | 432580 ko || -0m00.01s || -152 ko | -1.49% | -0.03% 0m00.66s | 443992 ko | Parsers/ContextFreeGrammar/Fold | 0m00.62s | 443884 ko || +0m00.04s || 108 ko | +6.45% | +0.02% 0m00.65s | 437384 ko | Parsers/Reachable/All/MinimalReachableOfReachable | 0m00.67s | 437348 ko || -0m00.02s || 36 ko | -2.98% | +0.00% 0m00.64s | 440304 ko | Parsers/ContextFreeGrammar/Fix/Definitions | 0m00.66s | 440512 ko || -0m00.02s || -208 ko | -3.03% | -0.04% 0m00.64s | 438688 ko | Parsers/Reachable/OnlyFirst/MinimalReachableOfReachable | 0m00.63s | 438672 ko || +0m00.01s || 16 ko | +1.58% | +0.00% 0m00.63s | 429040 ko | Common/Wf | 0m00.68s | 428912 ko || -0m00.05s || 128 ko | -7.35% | +0.02% 0m00.62s | 438484 ko | Parsers/ContextFreeGrammar/Properties | 0m00.60s | 438608 ko || +0m00.02s || -124 ko | +3.33% | -0.02% 0m00.62s | 442772 ko | Parsers/ContextFreeGrammar/ValidReflective | 0m00.61s | 442664 ko || +0m00.01s || 108 ko | +1.63% | +0.02% 0m00.62s | 441928 ko | Parsers/Reflective/Syntax | 0m00.58s | 441832 ko || +0m00.04s || 96 ko | +6.89% | +0.02% 0m00.62s | 483508 ko | Parsers/SimpleRecognizerOptimized | 0m00.65s | 483580 ko || -0m00.03s || -72 ko | -4.61% | -0.01% 0m00.61s | 431384 ko | Common/Ensembles/Morphisms | 0m00.66s | 431364 ko || -0m00.05s || 20 ko | -7.57% | +0.00% 0m00.59s | 440108 ko | ADTNotation/BuildADT | 0m00.56s | 440132 ko || +0m00.02s || -24 ko | +5.35% | -0.00% 0m00.59s | 434128 ko | Common/SumType | 0m00.56s | 434096 ko || +0m00.02s || 32 ko | +5.35% | +0.00% 0m00.59s | 444476 ko | Parsers/Reachable/OnlyLast/ReachableParse | 0m00.60s | 444424 ko || -0m00.01s || 52 ko | -1.66% | +0.01% 0m00.59s | 437780 ko | Parsers/Reachable/ParenBalanced/Core | 0m00.53s | 437672 ko || +0m00.05s || 108 ko | +11.32% | +0.02% 0m00.57s | 439088 ko | Parsers/ContextFreeGrammar/Carriers | 0m00.56s | 438944 ko || +0m00.00s || 144 ko | +1.78% | +0.03% 0m00.57s | 436220 ko | Parsers/ContextFreeGrammar/SimpleCorrectnessMorphisms | 0m00.57s | 436168 ko || +0m00.00s || 52 ko | +0.00% | +0.01% 0m00.56s | 420348 ko | Parsers/ContextFreeGrammar/Fix/PreInterface | 0m00.55s | 420088 ko || +0m00.01s || 260 ko | +1.81% | +0.06% 0m00.55s | 441592 ko | ADTRefinement/Refinements/ADTCache | 0m00.58s | 441212 ko || -0m00.02s || 380 ko | -5.17% | +0.08% 0m00.55s | 431764 ko | Common/i3list | 0m00.54s | 431844 ko || +0m00.01s || -80 ko | +1.85% | -0.01% 0m00.55s | 449108 ko | Parsers/GenericRecognizerEquality | 0m00.56s | 448932 ko || -0m00.01s || 176 ko | -1.78% | +0.03% 0m00.54s | 492584 ko | Parsers/ContextFreeGrammar/Fix/Interface | 0m00.53s | 492492 ko || +0m00.01s || 92 ko | +1.88% | +0.01% 0m00.53s | 444192 ko | Parsers/ContextFreeGrammar/ValidProperties | 0m00.66s | 444208 ko || -0m00.13s || -16 ko | -19.69% | -0.00% 0m00.53s | 496268 ko | Parsers/ParserImplementationOptimized | 0m00.54s | 496352 ko || -0m00.01s || -84 ko | -1.85% | -0.01% 0m00.53s | 443596 ko | Parsers/Reflective/Morphisms | 0m00.48s | 443560 ko || +0m00.05s || 36 ko | +10.41% | +0.00% 0m00.51s | 438832 ko | ADTRefinement/GeneralRefinements | 0m00.53s | 438964 ko || -0m00.02s || -132 ko | -3.77% | -0.03% 0m00.51s | 458096 ko | Parsers/Reflective/ParserLogicalRelations | 0m00.54s | 458060 ko || -0m00.03s || 36 ko | -5.55% | +0.00% 0m00.49s | 422312 ko | Common/String_as_OT | 0m00.52s | 422228 ko || -0m00.03s || 84 ko | -5.76% | +0.01% 0m00.49s | 432420 ko | Common/ilist2 | 0m00.48s | 432412 ko || +0m00.01s || 8 ko | +2.08% | +0.00% 0m00.49s | 460256 ko | Parsers/BooleanRecognizerCorrect | 0m00.50s | 460264 ko || -0m00.01s || -8 ko | -2.00% | -0.00% 0m00.49s | 443272 ko | Parsers/WellFoundedParseProperties | 0m00.48s | 443380 ko || +0m00.01s || -108 ko | +2.08% | -0.02% 0m00.48s | 441484 ko | ADTRefinement/GeneralBuildADTRefinements | 0m00.52s | 441420 ko || -0m00.04s || 64 ko | -7.69% | +0.01% 0m00.48s | 392992 ko | Parsers/Reachable/All/ReachableParse | 0m00.55s | 445196 ko || -0m00.07s || -52204 ko | -12.72% | -11.72% 0m00.47s | 441944 ko | Parsers/Reachable/MaybeEmpty/OfParse | 0m00.42s | 441816 ko || +0m00.04s || 128 ko | +11.90% | +0.02% 0m00.47s | 390572 ko | Parsers/Reachable/OnlyFirst/ReachableParse | 0m00.47s | 416456 ko || +0m00.00s || -25884 ko | +0.00% | -6.21% 0m00.46s | 442596 ko | ADTRefinement/BuildADTRefinements/RefineAllMethods | 0m00.50s | 442604 ko || -0m00.03s || -8 ko | -7.99% | -0.00% 0m00.46s | 439068 ko | ADTRefinement/Refinements/ADTRepInv | 0m00.45s | 438976 ko || +0m00.01s || 92 ko | +2.22% | +0.02% 0m00.46s | 428364 ko | Parsers/GenericRecognizerOptimizedTactics | 0m00.48s | 428248 ko || -0m00.01s || 116 ko | -4.16% | +0.02% 0m00.45s | 435556 ko | Common/FixedPoints | 0m00.47s | 435388 ko || -0m00.01s || 168 ko | -4.25% | +0.03% 0m00.45s | 435512 ko | Common/List/DisjointFacts | 0m00.43s | 435440 ko || +0m00.02s || 72 ko | +4.65% | +0.01% 0m00.44s | 432500 ko | Common/Gensym | 0m00.40s | 432432 ko || +0m00.03s || 68 ko | +9.99% | +0.01% 0m00.44s | 420476 ko | Common/LogicFacts | 0m00.45s | 420536 ko || -0m00.01s || -60 ko | -2.22% | -0.01% 0m00.44s | 360892 ko | Computation/Monad | 0m00.40s | 360616 ko || +0m00.03s || 276 ko | +9.99% | +0.07% 0m00.44s | 341184 ko | Parsers/ContextFreeGrammar/Equality | 0m00.44s | 341224 ko || +0m00.00s || -40 ko | +0.00% | -0.01% 0m00.44s | 506712 ko | Parsers/Refinement/ReductionTactics | 0m00.47s | 506172 ko || -0m00.02s || 540 ko | -6.38% | +0.10% 0m00.43s | 432528 ko | Common/ilist3 | 0m00.38s | 432464 ko || +0m00.04s || 64 ko | +13.15% | +0.01% 0m00.43s | 381724 ko | Parsers/SimpleBooleanRecognizerEquality | 0m00.41s | 381792 ko || +0m00.02s || -68 ko | +4.87% | -0.01% 0m00.43s | 365152 ko | Parsers/SimpleRecognizerExt | 0m00.41s | 365036 ko || +0m00.02s || 116 ko | +4.87% | +0.03% 0m00.41s | 412220 ko | ADTRefinement/BuildADTRefinements/AddCache | 0m00.38s | 412004 ko || +0m00.02s || 216 ko | +7.89% | +0.05% 0m00.41s | 410872 ko | ADTRefinement/Refinements/RefineHideADT | 0m00.37s | 410620 ko || +0m00.03s || 252 ko | +10.81% | +0.06% 0m00.41s | 433260 ko | Common/Sigma | 0m00.41s | 433368 ko || +0m00.00s || -108 ko | +0.00% | -0.02% 0m00.41s | 446212 ko | Parsers/BooleanRecognizerEquality | 0m00.45s | 446204 ko || -0m00.04s || 8 ko | -8.88% | +0.00% 0m00.41s | 445796 ko | Parsers/ParserADTSpecification | 0m00.44s | 445652 ko || -0m00.03s || 144 ko | -6.81% | +0.03% 0m00.41s | 389212 ko | Parsers/Reflective/ParserSemanticsOptimized | 0m00.39s | 389112 ko || +0m00.01s || 100 ko | +5.12% | +0.02% 0m00.40s | 431872 ko | ADTRefinement/Refinements/HoneRepresentation | 0m00.37s | 431708 ko || +0m00.03s || 164 ko | +8.10% | +0.03% 0m00.40s | 422296 ko | Common/Instances | 0m00.38s | 422276 ko || +0m00.02s || 20 ko | +5.26% | +0.00% 0m00.40s | 433344 ko | Common/List/Operations | 0m00.42s | 433400 ko || -0m00.01s || -56 ko | -4.76% | -0.01% 0m00.40s | 431356 ko | Common/ilist | 0m00.40s | 431380 ko || +0m00.00s || -24 ko | +0.00% | -0.00% 0m00.40s | 364860 ko | Parsers/BooleanRecognizerExt | 0m00.41s | 364660 ko || -0m00.00s || 200 ko | -2.43% | +0.05% 0m00.40s | 421784 ko | Parsers/GenericCorrectnessBaseTypes | 0m00.39s | 421800 ko || +0m00.01s || -16 ko | +2.56% | -0.00% 0m00.40s | 398816 ko | Parsers/GenericRecognizerCorrect | 0m00.47s | 400268 ko || -0m00.06s || -1452 ko | -14.89% | -0.36% 0m00.40s | 445780 ko | Parsers/ParserInterfaceReflective | 0m00.40s | 445392 ko || +0m00.00s || 388 ko | +0.00% | +0.08% 0m00.40s | 348796 ko | Parsers/Refinement/PreTactics | 0m00.40s | 348752 ko || +0m00.00s || 44 ko | +0.00% | +0.01% 0m00.40s | 438140 ko | Parsers/Reflective/PartialUnfold | 0m00.38s | 438208 ko || +0m00.02s || -68 ko | +5.26% | -0.01% 0m00.39s | 391720 ko | ADTRefinement/Core | 0m00.37s | 391368 ko || +0m00.02s || 352 ko | +5.40% | +0.08% 0m00.39s | 422328 ko | Common/SetEq | 0m00.36s | 422296 ko || +0m00.03s || 32 ko | +8.33% | +0.00% 0m00.39s | 421544 ko | Common/SetoidInstances | 0m00.38s | 421508 ko || +0m00.01s || 36 ko | +2.63% | +0.00% 0m00.39s | 432696 ko | Common/Telescope/Equality | 0m00.42s | 432716 ko || -0m00.02s || -20 ko | -7.14% | -0.00% 0m00.39s | 420920 ko | Common/UIP | 0m00.35s | 420920 ko || +0m00.04s || 0 ko | +11.42% | +0.00% 0m00.39s | 361076 ko | Computation/ApplyMonad | 0m00.39s | 360940 ko || +0m00.00s || 136 ko | +0.00% | +0.03% 0m00.39s | 422176 ko | Parsers/BaseTypesLemmas | 0m00.38s | 422140 ko || +0m00.01s || 36 ko | +2.63% | +0.00% 0m00.39s | 452244 ko | Parsers/BooleanRecognizerTests | 0m00.42s | 452108 ko || -0m00.02s || 136 ko | -7.14% | +0.03% 0m00.39s | 367896 ko | Parsers/ContextFreeGrammar/Reflective | 0m00.39s | 367976 ko || +0m00.00s || -80 ko | +0.00% | -0.02% 0m00.39s | 403532 ko | Parsers/Reflective/ParserSemantics | 0m00.39s | 403464 ko || +0m00.00s || 68 ko | +0.00% | +0.01% 0m00.38s | 420928 ko | Common/BoolFacts | 0m00.40s | 420924 ko || -0m00.02s || 4 ko | -5.00% | +0.00% 0m00.38s | 420500 ko | Common/Le | 0m00.38s | 420560 ko || +0m00.00s || -60 ko | +0.00% | -0.01% 0m00.38s | 430596 ko | Common/List/FlattenList | 0m00.42s | 430656 ko || -0m00.03s || -60 ko | -9.52% | -0.01% 0m00.38s | 370376 ko | Parsers/BooleanRecognizerFull | 0m00.37s | 370432 ko || +0m00.01s || -56 ko | +2.70% | -0.01% 0m00.38s | 435688 ko | Parsers/Grammars/JSON | 0m00.35s | 435524 ko || +0m00.03s || 164 ko | +8.57% | +0.03% 0m00.38s | 357256 ko | Parsers/Reachable/ParenBalanced/WellFounded | 0m00.32s | 357152 ko || +0m00.06s || 104 ko | +18.75% | +0.02% 0m00.38s | 344744 ko | Parsers/Reachable/ParenBalancedHiding/Core | 0m00.37s | 344568 ko || +0m00.01s || 176 ko | +2.70% | +0.05% 0m00.38s | 410156 ko | Parsers/Reflective/ParserSoundnessOptimized | 0m00.36s | 409920 ko || +0m00.02s || 236 ko | +5.55% | +0.05% 0m00.37s | 341664 ko | Common/Enumerable/BoolProp | 0m00.39s | 341836 ko || -0m00.02s || -172 ko | -5.12% | -0.05% 0m00.37s | 426464 ko | Common/Enumerable/ReflectiveForall | 0m00.38s | 426428 ko || -0m00.01s || 36 ko | -2.63% | +0.00% 0m00.37s | 403656 ko | Common/Enumerable/ReflectiveForallStaged | 0m00.37s | 403708 ko || +0m00.00s || -52 ko | +0.00% | -0.01% 0m00.37s | 357820 ko | Computation/FueledFix | 0m00.34s | 357572 ko || +0m00.02s || 248 ko | +8.82% | +0.06% 0m00.37s | 394128 ko | Computation/LogicLemmas | 0m00.37s | 394084 ko || +0m00.00s || 44 ko | +0.00% | +0.01% 0m00.37s | 399856 ko | Parsers/Reflective/ParserSoundness | 0m00.40s | 399780 ko || -0m00.03s || 76 ko | -7.50% | +0.01% 0m00.36s | 373872 ko | ADTInduction | 0m00.39s | 373596 ko || -0m00.03s || 276 ko | -7.69% | +0.07% 0m00.36s | 403684 ko | ADTRefinement/BuildADTSetoidMorphisms | 0m00.35s | 403740 ko || +0m00.01s || -56 ko | +2.85% | -0.01% 0m00.36s | 378264 ko | ADTRefinement/GeneralBuildADTTactics | 0m00.38s | 377956 ko || -0m00.02s || 308 ko | -5.26% | +0.08% 0m00.36s | 377476 ko | ADTRefinement/Refinements/SimplifyRep | 0m00.34s | 377556 ko || +0m00.01s || -80 ko | +5.88% | -0.02% 0m00.36s | 354540 ko | Common/Ensembles | 0m00.30s | 354268 ko || +0m00.06s || 272 ko | +20.00% | +0.07% 0m00.36s | 409748 ko | Common/Ensembles/Cardinal | 0m00.38s | 409872 ko || -0m00.02s || -124 ko | -5.26% | -0.03% 0m00.36s | 359132 ko | Computation/Core | 0m00.31s | 359312 ko || +0m00.04s || -180 ko | +16.12% | -0.05% 0m00.36s | 340216 ko | Parsers/ActionEvaluator | 0m00.33s | 340308 ko || +0m00.02s || -92 ko | +9.09% | -0.02% 0m00.36s | 421628 ko | Parsers/ContextFreeGrammar/SimpleTransfer | 0m00.40s | 421628 ko || -0m00.04s || 0 ko | -10.00% | +0.00% 0m00.36s | 435860 ko | Parsers/Grammars/JSONImpoverished | 0m00.40s | 435852 ko || -0m00.04s || 8 ko | -10.00% | +0.00% 0m00.36s | 435828 ko | Parsers/Grammars/JSONImpoverishedOriginal | 0m00.38s | 435968 ko || -0m00.02s || -140 ko | -5.26% | -0.03% 0m00.36s | 370816 ko | Parsers/Grammars/StringLiteral | 0m00.38s | 370724 ko || -0m00.02s || 92 ko | -5.26% | +0.02% 0m00.36s | 345328 ko | Parsers/Reflective/ParserPartialUnfold | 0m00.32s | 345472 ko || +0m00.03s || -144 ko | +12.49% | -0.04% 0m00.36s | 342480 ko | Parsers/Reflective/ParserSyntax | 0m00.30s | 342392 ko || +0m00.06s || 88 ko | +20.00% | +0.02% 0m00.36s | 349264 ko | Parsers/Reflective/Semantics | 0m00.37s | 349160 ko || -0m00.01s || 104 ko | -2.70% | +0.02% 0m00.36s | 347560 ko | Parsers/StringLike | 0m00.35s | 347768 ko || +0m00.01s || -208 ko | +2.85% | -0.05% 0m00.35s | 388308 ko | ADT/ComputationalADT | 0m00.39s | 387864 ko || -0m00.04s || 444 ko | -10.25% | +0.11% 0m00.35s | 376700 ko | ADT/Core | 0m00.30s | 376640 ko || +0m00.04s || 60 ko | +16.66% | +0.01% 0m00.35s | 388912 ko | ADTNotation/BuildADTReplaceMethods | 0m00.36s | 388832 ko || -0m00.01s || 80 ko | -2.77% | +0.02% 0m00.35s | 403116 ko | ADTNotation/BuildComputationalADT | 0m00.37s | 402816 ko || -0m00.02s || 300 ko | -5.40% | +0.07% 0m00.35s | 431700 ko | Common/i3list2 | 0m00.36s | 431632 ko || -0m00.01s || 68 ko | -2.77% | +0.01% 0m00.35s | 338920 ko | Computation | 0m00.34s | 338760 ko || +0m00.00s || 160 ko | +2.94% | +0.04% 0m00.35s | 356240 ko | Parsers/ContextFreeGrammar/Fix/Inject | 0m00.34s | 356200 ko || +0m00.00s || 40 ko | +2.94% | +0.01% 0m00.35s | 339876 ko | Parsers/ContextFreeGrammar/Notations | 0m00.33s | 339804 ko || +0m00.01s || 72 ko | +6.06% | +0.02% 0m00.35s | 339428 ko | Parsers/ContextFreeGrammar/PreNotations | 0m00.34s | 339372 ko || +0m00.00s || 56 ko | +2.94% | +0.01% 0m00.35s | 342320 ko | Parsers/ContextFreeGrammar/Precompute | 0m00.36s | 342200 ko || -0m00.01s || 120 ko | -2.77% | +0.03% 0m00.35s | 422232 ko | Parsers/ContextFreeGrammar/SimpleCorrectnessLemmas | 0m00.35s | 422236 ko || +0m00.00s || -4 ko | +0.00% | -0.00% 0m00.35s | 373952 ko | Parsers/Grammars/EvalGrammarTactics | 0m00.29s | 373960 ko || +0m00.06s || -8 ko | +20.68% | -0.00% 0m00.35s | 339112 ko | Parsers/Grammars/Trivial | 0m00.33s | 338776 ko || +0m00.01s || 336 ko | +6.06% | +0.09% 0m00.35s | 392892 ko | Parsers/Reflective/ParserReify | 0m00.38s | 393068 ko || -0m00.03s || -176 ko | -7.89% | -0.04% 0m00.35s | 415416 ko | Parsers/Reflective/SyntaxEquivalence | 0m00.37s | 415400 ko || -0m00.02s || 16 ko | -5.40% | +0.00% 0m00.34s | 398152 ko | Common/Prod | 0m00.36s | 398172 ko || -0m00.01s || -20 ko | -5.55% | -0.00% 0m00.34s | 370496 ko | Common/StringBound | 0m00.34s | 370288 ko || +0m00.00s || 208 ko | +0.00% | +0.05% 0m00.34s | 409944 ko | Common/i2list2 | 0m00.35s | 409764 ko || -0m00.00s || 180 ko | -2.85% | +0.04% 0m00.34s | 401088 ko | Common/ilist3_pair | 0m00.34s | 401184 ko || +0m00.00s || -96 ko | +0.00% | -0.02% 0m00.34s | 371972 ko | Parsers/ContextFreeGrammar/Fix/FromAbstractInterpretationDefinitionsRelations | 0m00.36s | 371724 ko || -0m00.01s || 248 ko | -5.55% | +0.06% 0m00.34s | 340276 ko | Parsers/ContextFreeGrammar/PreNotationsLemmas | 0m00.34s | 340264 ko || +0m00.00s || 12 ko | +0.00% | +0.00% 0m00.34s | 336604 ko | Parsers/ContextFreeGrammar/ReflectiveLemmas | 0m00.35s | 336648 ko || -0m00.00s || -44 ko | -2.85% | -0.01% 0m00.34s | 349824 ko | Parsers/Grammars/ExpressionParen | 0m00.30s | 349996 ko || +0m00.04s || -172 ko | +13.33% | -0.04% 0m00.34s | 342448 ko | Parsers/ParserInterface | 0m00.35s | 342368 ko || -0m00.00s || 80 ko | -2.85% | +0.02% 0m00.34s | 360816 ko | Parsers/Reachable/ParenBalancedHiding/WellFounded | 0m00.36s | 360808 ko || -0m00.01s || 8 ko | -5.55% | +0.00% 0m00.34s | 288120 ko | Parsers/Reflective/Reify | 0m00.35s | 288028 ko || -0m00.00s || 92 ko | -2.85% | +0.03% 0m00.33s | 343912 ko | ADT | 0m00.32s | 343904 ko || +0m00.01s || 8 ko | +3.12% | +0.00% 0m00.33s | 376912 ko | ADT/ADTHide | 0m00.33s | 376672 ko || +0m00.00s || 240 ko | +0.00% | +0.06% 0m00.33s | 348508 ko | ADTRefinement | 0m00.33s | 348044 ko || +0m00.00s || 464 ko | +0.00% | +0.13% 0m00.33s | 356944 ko | ADTRefinement/BuildADTRefinements | 0m00.36s | 356632 ko || -0m00.02s || 312 ko | -8.33% | +0.08% 0m00.33s | 347872 ko | ADTRefinement/Refinements | 0m00.30s | 347664 ko || +0m00.03s || 208 ko | +10.00% | +0.05% 0m00.33s | 385136 ko | ADTRefinement/Refinements/DelegateMethods | 0m00.32s | 384924 ko || +0m00.01s || 212 ko | +3.12% | +0.05% 0m00.33s | 360528 ko | Parsers/BooleanRecognizer | 0m00.33s | 360364 ko || +0m00.00s || 164 ko | +0.00% | +0.04% 0m00.33s | 341544 ko | Parsers/ContextFreeGrammar/TransferProperties | 0m00.34s | 341532 ko || -0m00.01s || 12 ko | -2.94% | +0.00% 0m00.33s | 378768 ko | Parsers/Grammars/ExpressionNumPlusParen | 0m00.36s | 378688 ko || -0m00.02s || 80 ko | -8.33% | +0.02% 0m00.33s | 365264 ko | Parsers/Grammars/JSComment | 0m00.31s | 365352 ko || +0m00.02s || -88 ko | +6.45% | -0.02% 0m00.33s | 335484 ko | Parsers/Reachable/All/Reachable | 0m00.35s | 335588 ko || -0m00.01s || -104 ko | -5.71% | -0.03% 0m00.33s | 335560 ko | Parsers/Reachable/OnlyFirst/ReachableWellFounded | 0m00.32s | 335804 ko || +0m00.01s || -244 ko | +3.12% | -0.07% 0m00.33s | 335624 ko | Parsers/Reachable/OnlyLast/ReachableWellFounded | 0m00.30s | 335760 ko || +0m00.03s || -136 ko | +10.00% | -0.04% 0m00.33s | 420268 ko | Parsers/StringLike/Core | 0m00.37s | 420456 ko || -0m00.03s || -188 ko | -10.81% | -0.04% 0m00.32s | 383020 ko | Common/Ensembles/Equivalence | 0m00.32s | 383176 ko || +0m00.00s || -156 ko | +0.00% | -0.04% 0m00.32s | 332152 ko | Common/Tactics/CacheStringConstant | 0m00.31s | 332156 ko || +0m00.01s || -4 ko | +3.22% | -0.00% 0m00.32s | 335676 ko | Computation/SetoidEqMorphisms | 0m00.31s | 335500 ko || +0m00.01s || 176 ko | +3.22% | +0.05% 0m00.32s | 382340 ko | Parsers/GenericRecognizer | 0m00.31s | 382404 ko || +0m00.01s || -64 ko | +3.22% | -0.01% 0m00.32s | 349688 ko | Parsers/Grammars/ABStar | 0m00.30s | 349584 ko || +0m00.02s || 104 ko | +6.66% | +0.02% 0m00.32s | 350776 ko | Parsers/Grammars/ExpressionNumPlus | 0m00.30s | 350788 ko || +0m00.02s || -12 ko | +6.66% | -0.00% 0m00.32s | 349088 ko | Parsers/Reflective/ParserSyntaxEquivalence | 0m00.34s | 349012 ko || -0m00.02s || 76 ko | -5.88% | +0.02% 0m00.32s | 280592 ko | Parsers/Reflective/Syntactify | 0m00.31s | 280744 ko || +0m00.01s || -152 ko | +3.22% | -0.05% 0m00.31s | 348544 ko | ADTNotation | 0m00.32s | 348308 ko || -0m00.01s || 236 ko | -3.12% | +0.06% 0m00.31s | 356680 ko | ADTNotation/BuildADTSig | 0m00.35s | 356312 ko || -0m00.03s || 368 ko | -11.42% | +0.10% 0m00.31s | 390284 ko | ADTRefinement/BuildADTRefinements/SimplifyRep | 0m00.33s | 390176 ko || -0m00.02s || 108 ko | -6.06% | +0.02% 0m00.31s | 385900 ko | Common/Monad | 0m00.30s | 386000 ko || +0m00.01s || -100 ko | +3.33% | -0.02% 0m00.31s | 378408 ko | Parsers/CorrectnessBaseTypes | 0m00.32s | 378416 ko || -0m00.01s || -8 ko | -3.12% | -0.00% 0m00.31s | 335092 ko | Parsers/Reachable/All/ReachableWellFounded | 0m00.34s | 335124 ko || -0m00.03s || -32 ko | -8.82% | -0.00% 0m00.31s | 334740 ko | Parsers/Reachable/MaybeEmpty/WellFounded | 0m00.30s | 334676 ko || +0m00.01s || 64 ko | +3.33% | +0.01% 0m00.31s | 336144 ko | Parsers/Reachable/OnlyLast/Reachable | 0m00.30s | 336116 ko || +0m00.01s || 28 ko | +3.33% | +0.00% 0m00.31s | 352792 ko | Parsers/Reflective/SemanticsOptimized | 0m00.34s | 352716 ko || -0m00.03s || 76 ko | -8.82% | +0.02% 0m00.31s | 377900 ko | Parsers/SimpleRecognizer | 0m00.29s | 377920 ko || +0m00.02s || -20 ko | +6.89% | -0.00% 0m00.31s | 330956 ko | Parsers/Specification | 0m00.32s | 330788 ko || -0m00.01s || 168 ko | -3.12% | +0.05% 0m00.30s | 360252 ko | Common/Ensembles/Tactics | 0m00.30s | 360084 ko || +0m00.00s || 168 ko | +0.00% | +0.04% 0m00.30s | 300272 ko | Common/EnumType | 0m00.32s | 300328 ko || -0m00.02s || -56 ko | -6.25% | -0.01% 0m00.30s | 388244 ko | Common/OptionFacts | 0m00.32s | 388204 ko || -0m00.02s || 40 ko | -6.25% | +0.01% 0m00.30s | 390184 ko | Common/Telescope/Instances | 0m00.30s | 390140 ko || +0m00.00s || 44 ko | +0.00% | +0.01% 0m00.30s | 360044 ko | Computation/Refinements/Tactics | 0m00.30s | 360152 ko || +0m00.00s || -108 ko | +0.00% | -0.02% 0m00.30s | 355812 ko | Parsers/Grammars/FlatComments | 0m00.34s | 355936 ko || -0m00.04s || -124 ko | -11.76% | -0.03% 0m00.29s | 376112 ko | ADT/ADTSig | 0m00.34s | 376084 ko || -0m00.05s || 28 ko | -14.70% | +0.00% 0m00.29s | 385280 ko | Common/SetoidClassInstances | 0m00.24s | 385360 ko || +0m00.04s || -80 ko | +20.83% | -0.02% 0m00.29s | 344152 ko | Parsers/ExtrOcamlPrimitives | 0m00.33s | 343948 ko || -0m00.04s || 204 ko | -12.12% | +0.05% 0m00.29s | 335512 ko | Parsers/Reachable/MaybeEmpty/Core | 0m00.29s | 335612 ko || +0m00.00s || -100 ko | +0.00% | -0.02% 0m00.29s | 336032 ko | Parsers/Reachable/OnlyFirst/Reachable | 0m00.32s | 336160 ko || -0m00.03s || -128 ko | -9.37% | -0.03% 0m00.28s | 253436 ko | Common/Coq__8_4__8_5__Compat | 0m00.28s | 253464 ko || +0m00.00s || -28 ko | +0.00% | -0.01% 0m00.28s | 386940 ko | Common/LogicMorphisms | 0m00.28s | 386844 ko || +0m00.00s || 96 ko | +0.00% | +0.02% 0m00.27s | 377148 ko | Common/PointedProp | 0m00.23s | 377220 ko || +0m00.04s || -72 ko | +17.39% | -0.01% 0m00.26s | 285368 ko | Common/LetIn | 0m00.21s | 285428 ko || +0m00.05s || -60 ko | +23.80% | -0.02% 0m00.26s | 269716 ko | Common/Tactics/FreeIn | 0m00.24s | 269704 ko || +0m00.02s || 12 ko | +8.33% | +0.00% 0m00.26s | 314552 ko | Parsers/Reachable/OnlyLast/MinimalReachable | 0m00.24s | 314472 ko || +0m00.02s || 80 ko | +8.33% | +0.02% 0m00.25s | 274432 ko | Common/Tactics/BreakMatch | 0m00.22s | 274588 ko || +0m00.03s || -156 ko | +13.63% | -0.05% 0m00.25s | 269888 ko | Common/Tactics/Head | 0m00.24s | 269840 ko || +0m00.01s || 48 ko | +4.16% | +0.01% 0m00.25s | 279656 ko | Common/VectorFacts | 0m00.25s | 279628 ko || +0m00.00s || 28 ko | +0.00% | +0.01% 0m00.25s | 338572 ko | Parsers/BaseTypes | 0m00.22s | 338856 ko || +0m00.03s || -284 ko | +13.63% | -0.08% 0m00.25s | 383804 ko | Parsers/GenericBoolCorrectnessBaseTypes | 0m00.29s | 383724 ko || -0m00.03s || 80 ko | -13.79% | +0.02% 0m00.25s | 311112 ko | Parsers/Reachable/MaybeEmpty/Minimal | 0m00.22s | 310980 ko || +0m00.03s || 132 ko | +13.63% | +0.04% 0m00.25s | 314444 ko | Parsers/Reachable/OnlyFirst/MinimalReachable | 0m00.25s | 314432 ko || +0m00.00s || 12 ko | +0.00% | +0.00% 0m00.24s | 298844 ko | Common/Match | 0m00.26s | 298860 ko || -0m00.02s || -16 ko | -7.69% | -0.00% 0m00.24s | 272412 ko | Common/Tactics/DestructHead | 0m00.22s | 272376 ko || +0m00.01s || 36 ko | +9.09% | +0.01% 0m00.24s | 300556 ko | Common/Telescope/Core | 0m00.23s | 300632 ko || +0m00.00s || -76 ko | +4.34% | -0.02% 0m00.24s | 269980 ko | Computation/Notations | 0m00.23s | 269840 ko || +0m00.00s || 140 ko | +4.34% | +0.05% 0m00.24s | 323744 ko | Parsers/ContextFreeGrammar/SimpleCorrectness | 0m00.23s | 323888 ko || +0m00.00s || -144 ko | +4.34% | -0.04% 0m00.24s | 269740 ko | Parsers/Grammars/JavaScriptExpression | 0m00.26s | 269744 ko || -0m00.02s || -4 ko | -7.69% | -0.00% 0m00.24s | 269692 ko | Parsers/Refinement/DisjointLemmasEarlyDeclarations | 0m00.24s | 269620 ko || +0m00.00s || 72 ko | +0.00% | +0.02% 0m00.24s | 270100 ko | Parsers/Refinement/DisjointRulesCommon | 0m00.21s | 270096 ko || +0m00.03s || 4 ko | +14.28% | +0.00% 0m00.23s | 272148 ko | Common/Tactics/DestructHyps | 0m00.24s | 272176 ko || -0m00.00s || -28 ko | -4.16% | -0.01% 0m00.23s | 270156 ko | Common/Tactics/FoldIsTrue | 0m00.22s | 270060 ko || +0m00.01s || 96 ko | +4.54% | +0.03% 0m00.23s | 321964 ko | Parsers/ContextFreeGrammar/Core | 0m00.24s | 321932 ko || -0m00.00s || 32 ko | -4.16% | +0.00% 0m00.23s | 321100 ko | Parsers/ContextFreeGrammar/Transfer | 0m00.26s | 320872 ko || -0m00.03s || 228 ko | -11.53% | +0.07% 0m00.23s | 328208 ko | Parsers/MinimalParse | 0m00.27s | 328200 ko || -0m00.04s || 8 ko | -14.81% | +0.00% 0m00.22s | 271340 ko | Common/Notations | 0m00.23s | 271352 ko || -0m00.01s || -12 ko | -4.34% | -0.00% 0m00.22s | 270020 ko | Common/ReservedNotations | 0m00.19s | 269932 ko || +0m00.03s || 88 ko | +15.78% | +0.03% 0m00.22s | 269712 ko | Common/Tactics/GetGoal | 0m00.22s | 269860 ko || +0m00.00s || -148 ko | +0.00% | -0.05% 0m00.22s | 269940 ko | Common/Tactics/PrintContext | 0m00.22s | 270112 ko || +0m00.00s || -172 ko | +0.00% | -0.06% 0m00.22s | 273176 ko | Common/Tactics/SetoidSubst | 0m00.20s | 273212 ko || +0m00.01s || -36 ko | +9.99% | -0.01% 0m00.22s | 270852 ko | Common/Tactics/SpecializeBy | 0m00.23s | 270968 ko || -0m00.01s || -116 ko | -4.34% | -0.04% 0m00.22s | 301156 ko | Parsers/ContextFreeGrammar/Valid | 0m00.22s | 300880 ko || +0m00.00s || 276 ko | +0.00% | +0.09% 0m00.22s | 300020 ko | Parsers/GenericBaseTypes | 0m00.24s | 299936 ko || -0m00.01s || 84 ko | -8.33% | +0.02% 0m00.22s | 269780 ko | Parsers/Grammars/JavaScriptStatementsWithoutAssignmentExpression | 0m00.26s | 269856 ko || -0m00.04s || -76 ko | -15.38% | -0.02% 0m00.22s | 312772 ko | Parsers/Reachable/All/MinimalReachable | 0m00.24s | 312944 ko || -0m00.01s || -172 ko | -8.33% | -0.05% 0m00.21s | 270932 ko | Common/Ensembles/Notations | 0m00.22s | 270964 ko || -0m00.01s || -32 ko | -4.54% | -0.01% 0m00.21s | 270440 ko | Common/Tactics/DestructSig | 0m00.21s | 270332 ko || +0m00.00s || 108 ko | +0.00% | +0.03% 0m00.21s | 269764 ko | Common/Tactics/IsClosed | 0m00.22s | 269600 ko || -0m00.01s || 164 ko | -4.54% | +0.06% 0m00.21s | 269148 ko | Parsers/BooleanRecognizerMin | 0m00.23s | 269244 ko || -0m00.02s || -96 ko | -8.69% | -0.03% 0m00.21s | 269612 ko | Parsers/Grammars/JavaScriptWithoutStatements | 0m00.21s | 269788 ko || +0m00.00s || -176 ko | +0.00% | -0.06% 0m00.21s | 311440 ko | Parsers/WellFoundedParse | 0m00.24s | 311400 ko || -0m00.03s || 40 ko | -12.50% | +0.01% 0m00.20s | 296800 ko | Common/StringOperations | 0m00.24s | 296700 ko || -0m00.03s || 100 ko | -16.66% | +0.03% 0m00.20s | 269980 ko | Common/Tactics/Combinators | 0m00.22s | 269972 ko || -0m00.01s || 8 ko | -9.09% | +0.00% 0m00.20s | 270788 ko | Common/Tactics/SplitInContext | 0m00.23s | 270800 ko || -0m00.03s || -12 ko | -13.04% | -0.00% 0m00.05s | 60256 ko | Common/Tactics/HintDbExtra | 0m00.04s | 60228 ko || +0m00.01s || 28 ko | +25.00% | +0.04% 0m00.04s | 60480 ko | Common/Tactics/TransparentAbstract | 0m00.04s | 60616 ko || +0m00.00s || -136 ko | +0.00% | -0.22% 0m00.03s | 23372 ko | Common/Tactics/hint_db_extra_tactics | 0m00.02s | 23320 ko || +0m00.00s || 52 ko | +49.99% | +0.22% 0m00.03s | 15716 ko | Common/Tactics/transparent_abstract_plugin | 0m00.03s | 15740 ko || +0m00.00s || -24 ko | +0.00% | -0.15% 0m00.02s | 15692 ko | Common/Tactics/hint_db_extra_plugin | 0m00.03s | 15744 ko || -0m00.00s || -52 ko | -33.33% | -0.33% 0m00.02s | 21960 ko | Common/Tactics/transparent_abstract_tactics | 0m00.02s | 22036 ko || +0m00.00s || -76 ko | +0.00% | -0.34% ```

JasonGross commented 3 years ago

So it seems like this PR gives us about a 14s speedup over the previous one, which itself did not have a meaningful impact on time.

mattam82 commented 3 years ago

Cool, thanks for checking!

mit-plv / fiat

Speed up morphism search of setoid-rewrite #53