[isabelle-dev] Antiquotation Parsing Time Increased between Isabelle 2017 and 2018
Makarius
makarius at sketis.net
Mon Apr 15 12:11:01 CEST 2019
On 15/04/2019 03:03, Jackson, Vincent (Data61, Kensington NSW) wrote:
>
> I recently ran into a performance degradation when updating some proofs to Isabelle 2018.
> These theory files involve a large number of anti-quotations in ML blocks.
>
> In Isabelle 2017 a file with ~1000 thm antiquotations takes 3 seconds; in Isabelle 2018, 2 minutes and 39 seconds.
>
> I have pinned down the source to this commit:
> d293958f9d use Poly/ML 5.7.1 test version as default;
>
> If anyone knows what changed to cause this, I'd be interested to know.
Included are the results of "isabelle -o profiling=time" and "isabelle
profiling_report .../heaps/.../log/Thy1024.gz" for Isabelle2017,
Isabelle2018, and the current approximation of Isabelle2019 (538919322852).
This shows that the time is spent in the Poly/ML compiler (by David
Matthews). The compiler has changed significantly in the past three
releases: 5.6, 5.7.1, 5.8 and it is again faster in this example.
Nonetheless the polyml-5.8 profile shows a significant entry:
16387 IntSet.mergeLists
It is up to David Matthews to say if this can be fine-tuned further.
BTW: in the ROOT file you have used session "Main", which is
documentation for theory Main in session "HOL". You should use session
"HOL" instead.
BTW 2: the isabelle-dev mailing list "covers the Isabelle development
process, including intermediate repository versions, and administrative
issues concerning the website or testing infrastructure" (quote from the
website). Anything else is for isabelle-users -- and the use of
Isabelle/ML is a normal Isabelle user activity.
BTW 3: you should follow official Isabelle releases as they are
published. In a few weeks you can already start working with
Isabelle2019-RC1 (feedback on that will be also on isabelle-users).
Makarius
-------------- next part --------------
Isabelle2017 contrib/polyml-5.6-1
Thy1024:
1 AList.map_index
1 Basics.fold
1 Scan.repeat
1 ML_Lex.gen_read
1 String.concat
1 CODETREE_STATIC_LINK_AND_CASES().staticLinkAndCases
1 X86OUTPUTCODE().checkBranchList
1 Substring.fields
1 CODEGEN_TABLE().moveToVec
1 ML_Env.sml_env
1 CODETREE_REMOVE_REDUNDANT().cleanProc
1 Thread_Attributes.uninterruptible
1 List.filter
1 Library.maps
1 Int.fmt
1 Multithreading.synchronized
1 Proofterm.fulfill_norm_proof
1 X86LOWLEVEL().loadToOneOf
1 Markup.markup
1 CODEGEN_TABLE().performActions
2 CODEGEN_TABLE().alignStack
2 List.map
2 List.@
3 CODETREE_SIMPLIFIER().simpSpecial
4 Table().defined
4 Table().lookup_key
4 CODEGEN_TABLE().indirect
4 UTILITIES_().noDuplicates
5 Axclass.insert_arity_completions
6 CODEGEN_TABLE().getRegisterInSet
8 CODEGEN_TABLE().clearCacheEntry
9 GARBAGE COLLECTION (minor collection)
9 GARBAGE COLLECTION (total)
9 MATCH_COMPILER().pattCode
11 CODEGEN_TABLE().pushRegisters
14 CODEGEN_TABLE().removeFromCache
16 CODEGEN_TABLE().saveState
19 StretchArray.update
23 CODEGEN_TABLE().removeOldItemsFromRealStack
28 CODEGEN_TABLE().mergeState
59 CODEGEN_TABLE().setState
103 CODETREE_STATIC_LINK_AND_CASES().lifeTimes
139 X86OPTIMISE().optimise
149 StretchArray.sub
-------------- next part --------------
Isabelle2018/contrib/polyml-5.7.1-8
Thy1024:
1 Symbol.bump_string
1 X86OUTPUTCODE().codeGenerate
1 Table().lookup
1 X86OPTIMISE().generateCode
1 Pretty.make_block
1 Future.scheduler_next
1 Thread.ConditionVar.innerWait
1 IntSet.partition
1 CODETREE_SIMPLIFIER().simpFunctionCall
1 Print_Mode.print_mode_value
1 X86ICodeToX86Code().icodeToX86Code
1 List.map
1 TYPE_TREE().tDisp
1 Command.reports_of_token
1 HashTable.hashSub
1 X86AllocateRegisters().allocateRegisters
1 X86CodetreeToICode().codeFunctionToX86
1 Symbol_Pos.explode_delete
1 Symbol_Pos.pad
1 Latex.output_positions
1 Thread_Attributes.uninterruptible
1 TYPE_TREE().copyTypeConstrWithCache
1 Proofterm.rewrite_prf
1 MATCH_COMPILER().constructorCode
1 Scan.finite'
1 String.implode
1 Symbol_Pos.!!!
1 Multithreading.synchronized
1 UNKNOWN
1 CODETREE_SIMPLIFIER().simpTuple
1 Parse.group
2 Scan.>>
2 Scan.||
2 List.@
3 Table().defined
4 GARBAGE COLLECTION (minor collection)
4 GARBAGE COLLECTION (total)
4 UTILITIES_().noDuplicates
5 X86ICodeIdentifyReferences().identifyRegisters
5 X86ICodeIdentifyReferences().getInstructionState
9 MATCH_COMPILER().pattCode
9 IntSet.minusLists
10 X86ICodeTransform().spillRegisters
174 IntSet.mergeLists
186 List.filter
16674 eq-cacheType
19110 X86PushRegisters().addRegisterPushes
-------------- next part --------------
Isabelle/538919322852 contrib/polyml-5.8
Thy1024:
1 ML_Antiquotation.gen_declaration
1 Scan.repeat
1 X86OPTIMISE().generateCode
1 Source.drain_source'
1 Future.scheduler_next
1 PolyCompareArbitrary
1 Scan.one
1 YXML.split_string
1 X86ICodeToX86Code().icodeToX86Code
1 CODETREE_CODEGEN_CONSTANT_FUNCTIONS().cgFuns
1 TYPE_TREE().tDisp
1 Symbol_Pos.source
1 X86CodetreeToICode().codeFunctionToX86
1 X86OUTPUTCODE().getConstant
1 ML_Env.make_name_space
1 Proofterm.rewrite_prf
1 STRUCTURES_().pass2Structs
1 CODETREE_FUNCTIONS().codeProps
1 CODETREE().genCode
1 Lazy.force_result
1 o
1 List.@
2 List.mapPartial
2 Table().lookup
2 LargeInt.fmt
2 Synchronized.value
3 UTILITIES_().noDuplicates
5 X86ICodeTransform().spillRegisters
5 GARBAGE COLLECTION (copy phase)
6 IntSet.partition
9 MATCH_COMPILER().pattCode
18 GARBAGE COLLECTION (update phase)
27 IntSet.addItem
29 X86PushRegisters().addRegisterPushes
35 X86ICodeIdentifyReferences().getInstructionState
39 List.foldr
48 IntSet.minusLists
80 List.map
89 UNKNOWN
94 eq-cacheType
96 GARBAGE COLLECTION (mark phase)
151 X86ICodeIdentifyReferences().identifyRegs
153 List.filter
255 X86ICodeOptimise().optimiseICode
385 GARBAGE COLLECTION (minor collection)
504 GARBAGE COLLECTION (total)
16387 IntSet.mergeLists
More information about the isabelle-dev
mailing list