Footex needs revision - Githubissues

GinoGiotto commented 1 year ago

I would like footex to be revisioned or splitted into less time-draining theorems. Most of the reasoning is already explained in #3269. Here I provide a little bit of data.

I made a script that executes the commands:

SHOW PROOF <label> /COMPRESSED
SHOW ELAPSED_TIME

For every theorem in main. From this I extracted the time-spans between two subsequent SHOW ELAPSED_TIME commands to get the duration of the corresponding show proof command.

This is the resulting graph. The x-axis represents the Nth theorem in main, while the y-axis shows the elapsed time (in seconds) from the previous SHOW ELAPSED_TIME command:

linear

This doesn't show much... let's make it logarithmic instead:

log

That's better. In this one the y-axis represents the elapsed time expressed in centiseconds (so in this graph 100 means 1 second).

That big spike that you see towards the end is indeed footex. That means that I waited 3028.67 seconds before getting an answer from it, which is around 50 minutes. The big spike of footex appears for other commands as well such as prove <label> or for the minimize command (I chose show proof because it's the quickest to work with, but my guess it's that the elapsed times for these commands are correlated).

Thanks to my minimization in #3269 footex's proof decreased from 2178 to 2161 steps (in the compressed format, with wff and repeated steps included), and as I already mentioned I think they are not enough to explain its time-draining property. For the record the highest amount of steps in main belongs to theorem 2503lem2, which has 5279 of them (the website shows a smaller count because it doesn't include wff and repeated steps), but it required only 0.51 seconds to output show proof 2503lem2 /compressed.

So the properties that make some theorems more time-challenging than others are an open question to me, I'm looking forward to hear your thoughts about it.

icecream17 commented 1 year ago

I quickly glanced over the code but I don't see any reason why this takes so long for footex. It shouldn't be because of any compressed proof expansion, looking at the code (and docs) it uses the compressed proof directly. (Incidentally the proof using the most compressed indices is fourierdlem103)

Relevant code for processing the show proof command: https://github.com/metamath/metamath-exe/blob/master/src/metamath.c#L3677

parseCompressedProof https://github.com/metamath/metamath-exe/blob/master/src/mmpars.c#L2735

(proof of footex for convenience)

``` ${ $d A a b d p q u v x y z $. $d C a b d p q u v x y z $. $d G a b d p q x y z $. $d I a b d p q x y z $. $d .- d p q x y z $. $d L a b d p q u v x y z $. $d P a b d p q x y z $. $d a b d p ph q x y z $. foot.x $e |- ( ph -> C e. P ) $. foot.y $e |- ( ph -> -. C e. A ) $. $( Lemma for ~ foot : existence part. (Contributed by Thierry Arnoux, 19-Oct-2019.) $) footex $p |- ( ph -> E. x e. A ( C L x ) ( perpG ` G ) A ) $= ( co wcel adantr va vb vy vp vz vq vd wceq wne cperpg cfv wbr wrex cmir cv eqid cstrkg ad3antrrr ad2antrr ad6antr simplr simprr eqcomd midexlem simp-4r simp-6r simprl ad4antr simp-5r simprd simp-7r ad10antr simp-11r wa simpllr necomd simp-9r simpld btwnlng3 lncom eleqtrrd nelne2 syl2anc wn eqnetrrd mirinv necon3bid mpbid tgcgrneq mirbtwn oveq1d tgbtwnouttr2 mircl tgbtwncom simplrl crag ccgrg oveq2d eqtrd israg mpbird tgcgrcomlr cs3 eqtr2d tglinerflx1 axtgcgrrflx axtg5seg trgcgr ragcgr eqidd krippen ragcom crn ad5antr ad9antr tglinethru tgelrnln tglinerflx2 elind mircgr simpr neeqtrd eleqtrd orcd ragcol eqeltrd wo btwncolg3 ragflat pm2.65da neneqd neqned ragperp reximssdv axtgsegcon r19.29a tgisline r19.29vva s3eqd ) ACUAUOZUBUOZHRZUHZYTUUAUIZVNZDBUOZHRZCFUJUKULZBCUMZUAUBEEAYTESZ VNZUUAESZVNZUUEVNZYTUUAUCUOZGRSZYTUUOIRZYTDIRZUHZVNZUUIUCEUUNUUOESZVNZU UTVNZDUUOUDUOZFUNUKZUKZUKZUHZUUIUDEUVCUVDESZVNZUVHVNZUUOYTUEUOZGRSZUUOU VLIRZUUOUVDIRZUHZVNZUUIUEEUVKUVLESZVNZUVQVNZUUOUVDUFUOZGRSZUUOUWAIRZUUO YTIRZUHZVNZUUIUFEUVTUWAESZVNZUWFVNZUUOUWAUVLUVEUKZUKZUGUOZGRSZUUOUWLIRZ UUODIRZUHZVNZUUIUGEUWIUWLESZVNZUWQVNZUWLDUUFUVEUKZUKZUHZUUHBCEUWTBDUWLU UOEUVEFGHUXAIJKLMUVEUPZUWIFUQSZUWRUWQUVTUXEUWGUWFUVKUXEUVRUVQUVCUXEUVIU VHUUNUXEUVAUUTAUXEUUJUULUUENURZUSZUSZUSZUSZUSZUXAUPZUWIDESZUWRUWQUVCUXM UVIUVHUVRUVQUWGUWFUUNUXMUVAUUTAUXMUUJUULUUEPURZUSZUTZUSZUWIUWRUWQVAUWIU VAUWRUWQUVTUVAUWGUWFUVKUVAUVRUVQUUNUVAUUTUVIUVHVEZUSZUSZUSZUWTUWNUWOUWS UWMUWPVBVCZVDUWTUUFESZUXCVNZVNZUUFUUOUVLHRCUYEEFGHUUOUVLUUFJLMUWTUXEUYD UXKTZUWTUVAUYDUYATZUWTUVRUYDUVKUVRUVQUWGUWFUWRUWQVFZTZUWTUYCUXCVGZUYEUU OUVDUUOUVLEFGIJKLUYFUYGUWTUVIUYDUVTUVIUWGUWFUWRUWQUVCUVIUVHUVRUVQVEZVHZ TZUYGUYIUWTUVOUVNUHUYDUWTUVNUVOUWTUVMUVPUVSUVQUWGUWFUWRUWQVIZVJVCZTUYEU VDUUOUYEUVGUUOUIUVDUUOUIUYEDUVGUUOUWTUVHUYDUVJUVHUVRUVQUWGUWFUWRUWQVKZT ZUYEUUODUYEUUOCSZDCSWDZUUODUIUWTUYRUYDUWTUUOUUBCUWTEFGHYTUUAUUOJLMUXKUV TUUJUWGUWFUWRUWQUVKUUJUVRUVQUVCUUJUVIUVHUUNUUJUVAUUTAUUJUULUUEVOZUSZUSZ USZVHZUUNUULUVAUUTUVIUVHUVRUVQUWGUWFUWRUWQUUKUULUUEVAZVLZUYAUWTUUCUUDUU MUUEUVAUUTUVIUVHUVRUVQUWGUWFUWRUWQVMZVJZUWTEFGHUUAYTUUOJLMUXKVUFVUDUYAU WTYTUUAVUHVPUWTUUPUUSUVBUUTUVIUVHUVRUVQUWGUWFUWRUWQVQZVRVSVTUWTUUCUUDVU GVRZWATZUWTUYSUYDUUNUYSUVAUUTUVIUVHUVRUVQUWGUWFUWRUWQAUYSUUJUULUUEQURVL ZTZUUODCWBWCVPZWEUYEUVGUUOUVDUUOUYEUVDUUOEUVEFGHUVFIJKLMUXDUYFUYMUVFUPZ UYGWFWGWHZVPZWIZUYEEFGHUVLUUOUUFJLMUYFUYIUYGUYJUYEUUOUVLVURVPZUYEUWAUWK UUOEUVEDUWLFGHUWJIUXAUVLUUFJKLMUXDUYFUWJUPZUXLUWTUWGUYDUVTUWGUWFUWRUWQV EZTZUWIUWKESUWRUWQUYDUWIUVLEUVEFGHUWJIUWAJKLMUXDUXJUVKUVRUVQUWGUWFVEVUT UVTUWGUWFVAWMZURZUYGUWTUXMUYDUXQTZUWIUWRUWQUYDVOZUYIUYJUYEDUUOUWAEFGIJK LUYFVVEUYGVVBUYEDUVDUUOUWAEFGIJKLUYFVVEUYMUYGVVBVUPUYEUVDUVGUUOGRDUUOGR UYEUVDUUOEUVEFGHUVFIJKLMUXDUYFUYMVUOUYGWJUYEDUVGUUOGUYQWKWAZUWTUWBUYDUW TUWBUWEUWHUWFUWRUWQVOZVRZTWLWNZUWSUWMUWPUYDWOZUWTUWCUUOUWKIRUHZUYDUWTUU OUVLUWAXCFWPUKZSVVLUWTUWAUVLUUOEUVEFGHIJKLMUXDUXKVVAUYHUYAUWTYTUVDUUOUW AEFWQUKZUVEUVLUUOFGHIJKLMUXDUXKVUDUYLUYAVVNUPZVVAUYHUYAUWTYTUVDUUOXCVVM SZUUQYTUVGIRZUHUWTUUQUURVVQUWTUUPUUSVUIVJZUWTDUVGYTIUYPWRWSUWTYTUVDUUOE UVEFGHIJKLMUXDUXKVUDUYLUYAWTXAZUWTYTUVDUUOUWAEVVNUVLUUOFIJKVVOUXKVUDUYL UYAVVAUYHUYAUWTUVDYTUVLUWAEFGIJKLUXKUYLVUDUYHVVAUWTYTUUOUVLEYTFGIUWAUWA UUOUVDJKLUXKVVAUYAUYLVUDUYAUYHVUDVVAUWTUUOUWAUWTDYTUUOUWAEFGIJKLUXKUXQV UDUYAVVAUWTUWCUWDDYTIRUWTUWBUWEVVHVJZUWTYTUUOYTDEFGIJKLUXKVUDUYAVUDUXQV VRXBXDUWTYTDUWTYTCSZUYSYTDUIZUWTYTUUBCUWTEYTUUAFGHJLMUXKVUDVUFVUHXEVUJW AZVULYTDCWBWCZVPWIVPZUWTUVDUUOUWAEFGIJKLUXKUYLUYAVVAVVIWNUWTUVMUVPUYNVR ZUWTUUOUWAUUOYTEFGIJKLUXKUYAVVAUYAVUDVVTXBUYOUWTEFGIUWAYTJKLUXKVVAVUDXF UWTUWCUWDVVTVCZXGXBUWTUUOUVDUUOUVLEFGIJKLUXKUYAUYLUYAUYHUYOXBVWGXHXIXLU WTUUOUVLUWAEUVEFGHIJKLMUXDUXKUYAUYHVVAWTWHTZUWTUWOUWNUHUYDUYBTZUYEUWKXJ UWTUYCUXCVBZXKVSVTUYECEUUOUVLFGHJLMUYFUYGUYIVURVURUVCCHXMSZUVIUVHUVRUVQ UWGUWFUWRUWQUYDAVWKUUJUULUUEUVAUUTOXNXOZVUKUYEUVLYTUUOHRZCUYEEFGHYTUUOU VLJLMUYFUWTUUJUYDVUDTZUYGUYIUYEYTDYTUUOEFGIJKLUYFVWNVVEVWNUYGUYEUUQUURU WTUUSUYDVVRTVCZUWTVWBUYDVWDTZWIZUWTUVMUYDVWFTVSZUYECEYTUUOFGHJLMUYFVWNU YGVWQVWQVWLUWTVWAUYDVWCTVUKXPWAXPWAZUYEUUGCEDFGHIUUOUUFJKLMUYFUYEEFGHDU UFJLMUYFVVEUYJUYEUUFDUYEUUFCSUYSUUFDUIVWSVUMUUFDCWBWCVPZXQVWLUYEUUGCUUF UYEEDUUFFGHJLMUYFVVEUYJVWTXRVWSXSUYEEDUUFFGHJLMUYFVVEUYJVWTXEVUKVWTUYEU UOUUFUYEUUOUUFUHZUUOUVDUHZUYEVXAVNZYTUUOUVDEUVEFGHIJKLMUXDUYEUXEVXAUYFT ZUYEUUJVXAVWNTZUYEUVAVXAUYGTZUYEUVIVXAUYMTZVXCUVDUUOYTEUVEFGHIJKLMUXDVX DVXGVXFVXEVXCDUUOYTUVDEUVEFGHIJKLMUXDVXDUYEUXMVXAVVETZVXFVXEVXGVXCDUUOY TXCDUUFYTXCVVMVXCDUUOYTYTDUUFVXCDXJUYEVXAYAZVXCYTXJYSVXCYTUUFDEUVEFGHIJ KLMUXDVXDVXEUYEUYCVXAUYJTZVXHVXCUVLUUFDYTEUVEFGHIJKLMUXDVXDUYEUVRVXAUYI TZVXJVXHVXEUYEUVLUUFDXCVVMSZVXAUYEVXLUVLDIRZUVLUXBIRZUHUYEVXMUVLUWLIRVX NUYEDUVLUWLUVLEFGIJKLUYFVVEUYIVVFUYIUYEUWKUUOUWLEUVLFGIUVLUWAUUODJKLUYF VVBUYGVVEVVDUYGVVFUYIUYIUWTUWAUUOUIUYDVWETVVJVVKUYEUUOUWAUUOUWKEFGIJKLU YFUYGVVBUYGVVDVWHXBVWIUYEUVLUWAUVLUWKEFGIJKLUYFUYIVVBUYIVVDUYEUVLUWKIRU VLUWAIRUYEUVLUWAEUVEFGHUWJIJKLMUXDUYFUYIVUTVVBXTVCXBUYEUVNXJXGXBUYEUWLU XBUVLIVWJWRWSUYEUVLUUFDEUVEFGHIJKLMUXDUYFUYIUYJVVEWTXATVXCUVLUUOUUFUYEU VLUUOUIVXAVUSTVXIYBVXCUVLUUFYTHRZSUUFYTUHVXCUVLUUOYTHRVXOVXCEFGHUUOYTUV LJLMVXDVXFVXEVXKVXCYTUUOVXCYTDYTUUOEFGIJKLVXDVXEVXHVXEVXFUYEUURUUQUHVXA VWOTUYEVWBVXAVWPTWIVPUYEUVLVWMSVXAVWRTVTVXCUUOUUFYTHVXIWKYCYDYEXLYFUYED UUOUIVXAVUNTUYEDUUOUVDHRSVXBYGVXAUYEEFGHUUOUVDDJMLUYFUYGUYMVVEUYEDUVDUU OEFGIJKLUYFVVEUYMUYGVVGWNYHTYEXLUWTVVPUYDVXAVVSUSYIVXCUUOUVDUYEUUOUVDUI VXAVUQTYKYJYLUYEUUOUUFDEUVEFGHIJKLMUXDUYFUYGUYJVVEUYEUUOUUFDXCVVMSUWOUU OUXBIRZUHUYEUWOUWNVXPVWIUYEUWLUXBUUOIVWJWRWSUYEUUOUUFDEUVEFGHIJKLMUXDUY FUYGUYJVVEWTXAXLYMYNUWIUGUUODEFGIUWKUUOJKLUXJVVCUXTUXTUXPYOYPUVTUFUUOYT EFGIUVDUUOJKLUXIUYKUXSUXSVUCYOYPUVKUEUUOUVDEFGIYTUUOJKLUXHVUBUXRUXRUVCU VIUVHVAYOYPUVCUDUUODYTEUVEFGHUVFIJKLMUXDUXGVUOUUNUVAUUTVAUXOVUAUVBUUPUU SVBVDYPUUNUCYTDEFGIUUAYTJKLUXFVUEUYTUYTUXNYOYPAUAUBCEFGHJLMNOYQYR $} ```

Speculation on why footex takes so long that doesn't work because it doesn't explain why show proof would also take so long

[I said](https://github.com/metamath/set.mm/pull/3269#issuecomment-1611674316) this reminded me of 4syl's comment. 4syl is a theorem that could be tried against any combination of four implications, so I'm guessing maybe that's why 4syl would extend minimize so long. Similarly, footex is one of two theorems using [ad10antr](https://us.metamath.org/mpeuni/ad10antr.html) with more than 2 website steps. In steps with many antecedents, there are many ad*ant*r theorems that would fit. Maybe it's all these valid combinations that takes so long? ![image](https://github.com/metamath/set.mm/assets/58114641/481a8fd1-0aa9-4283-ab41-c840ea331581) Here, one could easily use ad4antr, ad5antr, ..., ad10antr, and it would be valid. But it turns out all of these steps are also needed somewhere else. (Incidentally, footex is the only theorem using simp-11r)

GinoGiotto commented 1 year ago

I'm guessing, but might be related to the deduplication algorithm discussed in https://github.com/metamath/set.mm/pull/3195#issuecomment-1556312680?

If I write SHOW PROOF footex /COMPRESSED /FAST or SAVE PROOF footex /COMPRESSED /FAST then it responds very quickly, but without the /FAST option they both require a lot of time to process.

icecream17 commented 1 year ago

Interesting. So I would guess the MINIMIZE command uses the non-compressed version of the proof. Maybe that's why it takes so long - it retries all the duplicate subproofs

GinoGiotto commented 1 year ago

I did the same thing, but with the /FAST option. So I submitted these commands for every theorem in main:

SHOW PROOF <label> /COMPRESSED /FAST
SHOW ELAPSED_TIME

This is the resulting graph. This time the graph is linear and the y-axis is measured in seconds: fast

Here footex is no longer the slowest one, it needed only 0.26 seconds to return an answer. The gold medal (more like the worst medal) belongs to mdetunilem9, which required 0.59 seconds to execute the command.

GinoGiotto commented 1 year ago

I did a second run with the /FAST option, so I executed again:

SHOW PROOF <label> /COMPRESSED /FAST
SHOW ELAPSED_TIME

fast1

The resulting graph is somewhat similar, but not exacly identical to the previous one. This means that there are fluctuations. Anyway I don't think we need to be super accurate, what matters is that footex is no longer out of scale (it measures 0.25 seconds this time).

Theorem mdetunilem9 still has the gold medal with 0.60 seconds, so that seems to be consistent.

savask commented 1 year ago

@GinoGiotto As an idea, you could try compiling metamath-exe with profiling support and seeing what procedure(s) take the most of time when loading footex.

GinoGiotto commented 1 year ago

@GinoGiotto As an idea, you could try compiling metamath-exe with profiling support and seeing what procedure(s) take the most of time when loading footex.

Could you elaborate more? I'm not sure if this falls within the scope of my capabilities.

savask commented 1 year ago

Could you elaborate more? I'm not sure if this falls within the scope of my capabilities.

I'm assuming you're compiling metamath-exe by yourself, instead of using an already precompiled executable. If yes, then the rough instructions are as follows: 1) Supply -pg option to the gcc compiler 2) Run the program. 3) After it finishes, run gprof ./metamath to see the profiling results.

If you google "gcc profiling" and "gprof", you'll see better explanations.

GinoGiotto commented 1 year ago

@savask Ok, so I submitted the following commands on metamath.exe:

set scroll continuous
read set.mm
show proof footex /compressed

This is the time report after running gprof metamath.exe:

Flat profile:

Each sample counts as 0.01 seconds.
  %   cumulative   self              self     total
 time   seconds   seconds    calls  Ks/call  Ks/call  name
 82.36   1968.38  1968.38  4883242     0.00     0.00  nmbrCpy
 17.47   2385.93   417.55  1304208     0.00     0.00  nmbrNCpy
  0.02   2386.44     0.51 11109595     0.00     0.00  nmbrLen
  0.02   2386.90     0.46  2866829     0.00     0.00  memFreePoolPurge
  0.02   2387.30     0.40  4492743     0.00     0.00  poolFree
  0.01   2387.57     0.27   976996     0.00     0.00  nmbrLet
  0.01   2387.76     0.19  4883645     0.00     0.00  nmbrTempAlloc
  0.01   2387.93     0.17        1     0.00     0.00  parseStatements
  0.01   2388.09     0.16 10360745     0.00     0.00  rawWhiteSpaceLen
  0.01   2388.24     0.15   649376     0.00     0.00  nmbrInstr
  0.01   2388.38     0.14      118     0.00     0.00  countLines
  0.01   2388.51     0.14        1     0.00     1.61  nmbrSquishProof
  0.01   2388.66     0.14        1     0.00     0.00  readRawSource
  0.01   2388.79     0.14  3906950     0.00     0.00  poolMalloc
  0.01   2388.92     0.13   329465     0.00     0.00  nmbrGetSubproofLen
  0.00   2389.03     0.11 10360745     0.00     0.00  rawTokenLen
  0.00   2389.14     0.11   976570     0.00     0.00  nmbrCat
  0.00   2389.23     0.09        1     0.00     0.78  nmbrUnsquishProof
  0.00   2389.30     0.07   649291     0.00     0.00  nmbrAddElement
  0.00   2389.37     0.07        1     0.00     0.00  parseKeywords
  0.00   2389.43     0.06      109     0.00     0.00  getNextInclusion
  0.00   2389.49     0.06        1     0.00     0.00  eraseSource
  0.00   2389.55     0.06                             mathSrchCmp
  0.00   2389.60     0.05   976569     0.00     0.00  nmbrRight
  0.00   2389.65     0.05        1     0.00     2.39  command
  0.00   2389.70     0.04   976570     0.00     0.00  nmbrLeft
  0.00   2389.72     0.03  2560399     0.00     0.00  whiteSpaceLen
  0.00   2389.76     0.03  2560291     0.00     0.00  tokenLen
  0.00   2389.78     0.02        2     0.00     0.00  nmbrMakeTempAlloc
  0.00   2389.79     0.01                             labelSortCmp
  0.00   2389.80     0.01     4462     0.00     0.00  nmbrElementIn
  0.00   2389.81     0.01        1     0.00     0.00  parseLabels
  0.00   2389.82     0.01                             free
  0.00   2389.83     0.01                             isgraph
  0.00   2389.84     0.01                             malloc
  0.00   2389.85     0.01                             mathSortCmp
  0.00   2389.86     0.01                             labelSrchCmp
  0.00   2389.86     0.01                             nmbrMid
  0.00   2389.86     0.00   976996     0.00     0.00  nmbrAllocLen
  0.00   2389.86     0.00   585793     0.00     0.00  poolFixedMalloc
  0.00   2389.86     0.00   327638     0.00     0.00  nmbrSeg
  0.00   2389.86     0.00   171977     0.00     0.00  freeTempAlloc
  0.00   2389.86     0.00    86554     0.00     0.00  let
  0.00   2389.86     0.00    41409     0.00     0.00  instr
  0.00   2389.86     0.00    40898     0.00     0.00  entry
  0.00   2389.86     0.00    40898     0.00     0.00  matches
  0.00   2389.86     0.00    40898     0.00     0.00  matchesList
  0.00   2389.86     0.00    40898     0.00     0.00  numEntries
  0.00   2389.86     0.00     1178     0.00     0.00  pntrLen
  0.00   2389.86     0.00      924     0.00     0.00  cat
  0.00   2389.86     0.00      705     0.00     0.00  mid
  0.00   2389.86     0.00      471     0.00     0.00  pntrTempAlloc
  0.00   2389.86     0.00      416     0.00     0.00  seg
  0.00   2389.86     0.00      404     0.00     0.00  pntrCpy
  0.00   2389.86     0.00      289     0.00     0.00  left
  0.00   2389.86     0.00      287     0.00     0.00  nmbrZapLen
  0.00   2389.86     0.00      258     0.00     0.00  pntrAllocLen
  0.00   2389.86     0.00      258     0.00     0.00  pntrLet
  0.00   2389.86     0.00      191     0.00     0.00  pntrAddElement
  0.00   2389.86     0.00      149     0.00     0.00  len
  0.00   2389.86     0.00      125     0.00     0.00  cmdMatches
  0.00   2389.86     0.00      124     0.00     0.00  chr
  0.00   2389.86     0.00      106     0.00     0.00  proofTokenLen
  0.00   2389.86     0.00       93     0.00     0.00  print2
  0.00   2389.86     0.00       86     0.00     0.00  right
  0.00   2389.86     0.00       38     0.00     0.00  addToUsedPool
  0.00   2389.86     0.00       36     0.00     0.00  switchPos
  0.00   2389.86     0.00       18     0.00     0.00  string
  0.00   2389.86     0.00       15     0.00     0.00  pntrLeft
  0.00   2389.86     0.00       15     0.00     0.00  pntrNCpy
  0.00   2389.86     0.00       15     0.00     0.00  space
  0.00   2389.86     0.00       13     0.00     0.00  alloc2DMatrix
  0.00   2389.86     0.00       13     0.00     0.00  free2DMatrix
  0.00   2389.86     0.00       13     0.00     0.00  knapsack01
  0.00   2389.86     0.00       11     0.00     0.00  edit
  0.00   2389.86     0.00       11     0.00     0.00  nmbrSpace
  0.00   2389.86     0.00        9     0.00     0.00  lastArgMatches
  0.00   2389.86     0.00        7     0.00     0.00  pntrSpace
  0.00   2389.86     0.00        4     0.00     0.00  cmdInput
  0.00   2389.86     0.00        4     0.00     0.00  cmdInput1
  0.00   2389.86     0.00        4     0.00     0.00  parseCommandLine
  0.00   2389.86     0.00        4     0.00     0.00  processCommandLine
  0.00   2389.86     0.00        2     0.00     0.00  compareDates
  0.00   2389.86     0.00        2     0.00     0.00  eraseTexDefs
  0.00   2389.86     0.00        2     0.00     0.00  getContrib
  0.00   2389.86     0.00        2     0.00     0.00  getSourceIndentation
  0.00   2389.86     0.00        2     0.00     0.00  initBigArrays
  0.00   2389.86     0.00        2     0.00     0.00  makeTempAlloc
  0.00   2389.86     0.00        2     0.00     0.00  printLongLine
  0.00   2389.86     0.00        2     0.00     0.00  rinstr
  0.00   2389.86     0.00        1     0.00     0.00  compressProof
  0.00   2389.86     0.00        1     0.00     0.00  fSafeOpen
  0.00   2389.86     0.00        1     0.00     0.00  freeCommandLine
  0.00   2389.86     0.00        1     0.00     0.00  freeData
  0.00   2389.86     0.00        1     0.00     0.00  freeInOu
  0.00   2389.86     0.00        1     0.00     0.00  getDescription
  0.00   2389.86     0.00        1     0.00     0.00  getMarkupFlag
  0.00   2389.86     0.00        1     0.00     0.00  nmbrCvtRToVString
  0.00   2389.86     0.00        1     0.00     0.00  nmbrUnion
  0.00   2389.86     0.00        1     0.00     0.00  parseCompressedProof
  0.00   2389.86     0.00        1     0.00     0.00  parseMathDecl
  0.00   2389.86     0.00        1     0.00     0.00  parseProof
  0.00   2389.86     0.00        1     0.00     0.00  readFileToString
  0.00   2389.86     0.00        1     0.00     0.00  readInclude
  0.00   2389.86     0.00        1     0.00     0.00  readInput
  0.00   2389.86     0.00        1     0.00     0.00  readSourceAndIncludes
  0.00   2389.86     0.00        1     0.00     0.00  str

 %         the percentage of the total running time of the
time       program used by this function.

cumulative a running sum of the number of seconds accounted
 seconds   for by this function and those listed above it.

 self      the number of seconds accounted for by this
seconds    function alone.  This is the major sort for this
           listing.

calls      the number of times this function was invoked, if
           this function is profiled, else blank.

 self      the average number of milliseconds spent in this
ms/call    function per call, if this function is profiled,
           else blank.

 total     the average number of milliseconds spent in this
ms/call    function and its descendents per call, if this
           function is profiled, else blank.

name       the name of the function.  This is the minor sort
           for this listing. The index shows the location of
           the function in the gprof listing. If the index is
           in parenthesis it shows where it would appear in
           the gprof listing if it were to be printed.
♀
Copyright (C) 2012-2017 Free Software Foundation, Inc.

Copying and distribution of this file, with or without modification,
are permitted in any medium without royalty provided the copyright
notice and this notice are preserved.
♀

The commands set scroll continuous and read set.mm together require around one second of computing time, so I don't think we need to worry about their influence.

Looking at the report, it appears that the most problematic procedures are nmbrCpy and nmbrNCpy. However, I am not familiar enough with the code to understand their functionality.

There is also a table that says to describe the call tree of the program, are you interested in that as well?

savask commented 1 year ago

There is also a table that says to describe the call tree of the program, are you interested in that as well?

A call tree might be useful. I think it should show that nmbrUnsquishProof takes a lot of time, if my guess is correct that the problem is with unpacking.

GinoGiotto commented 1 year ago

@savask

                     Call graph (explanation follows)

granularity: each sample hit covers 4 byte(s) for 0.00% of 2389.86 seconds

index % time    self  children    called     name
                                                 
[1]    100.0    0.00 2389.73                 main [1]
                0.05 2389.68       1/1           command [2]
                0.00    0.00       2/93          print2 [61]
                0.00    0.00       1/15          space [93]
                0.00    0.00       1/2           initBigArrays [103]
                0.00    0.00       1/86554       let [70]
-----------------------------------------------
                0.05 2389.68       1/1           main [1]
[2]    100.0    0.05 2389.68       1         command [2]
                0.14 1606.08       1/1           nmbrSquishProof [4]
                0.09  782.29       1/1           nmbrUnsquishProof [6]
                0.00    0.92       1/1           readInput [14]
                0.06    0.05       1/1           eraseSource [28]
                0.00    0.03       1/1           compressProof [34]
                0.00    0.01       4/4           parseCommandLine [43]
                0.00    0.01      19/976996      nmbrLet [8]
                0.00    0.00       1/1           freeCommandLine [48]
                0.00    0.00       1/4462        nmbrElementIn [38]
                0.00    0.00      12/258         pntrLet [52]
                0.00    0.00       4/4           cmdInput1 [56]
                0.00    0.00       1/2           getContrib [55]
                0.00    0.00       4/4           processCommandLine [58]
                0.00    0.00       1/1           parseProof [59]
                0.00    0.00       2/2           printLongLine [62]
                0.00    0.00       4/11109595     nmbrLen [16]
                0.00    0.00       1/1           freeData [64]
                0.00    0.00       1/1           freeInOu [65]
                0.00    0.00       4/93          print2 [61]
                0.00    0.00   40898/40898       matchesList [74]
                0.00    0.00      83/86554       let [70]
                0.00    0.00      51/125         cmdMatches [85]
                0.00    0.00      36/36          switchPos [90]
                0.00    0.00      12/1178        pntrLen [76]
                0.00    0.00       4/924         cat [77]
                0.00    0.00       2/15          space [93]
                0.00    0.00       1/2           eraseTexDefs [101]
                0.00    0.00       1/1           fSafeOpen [106]
                0.00    0.00       1/2           getSourceIndentation [102]
                0.00    0.00       1/1           str [110]
-----------------------------------------------
                0.00    0.00       1/4883242     nmbrUnion [44]
              261.72    0.00  649291/4883242     nmbrAddElement [11]
              393.64    0.00  976568/4883242     nmbrRight [9]
              393.80    0.00  976954/4883242     nmbrLet [8]
              919.21    0.00 2280428/4883242     nmbrCat [5]
[3]     82.4 1968.38    0.00 4883242         nmbrCpy [3]
-----------------------------------------------
                0.14 1606.08       1/1           command [2]
[4]     67.2    0.14 1606.08       1         nmbrSquishProof [4]
                0.07  611.39  649280/976570      nmbrCat [5]
                0.18  262.08  649635/976996      nmbrLet [8]
                0.07  261.92  649280/649291      nmbrAddElement [11]
                0.03  261.92  649280/976569      nmbrRight [9]
                0.03  208.04  649280/976570      nmbrLeft [10]
                0.15    0.06  649376/649376      nmbrInstr [23]
                0.00    0.11     351/327638      nmbrSeg [12]
                0.01    0.00       1/2           nmbrMakeTempAlloc [35]
                0.00    0.00    2178/329465      nmbrGetSubproofLen [27]
                0.00    0.00     256/11109595     nmbrLen [16]
-----------------------------------------------
                0.00    0.00       3/976570      compressProof [34]
                0.04  308.19  327287/976570      nmbrUnsquishProof [6]
                0.07  611.39  649280/976570      nmbrSquishProof [4]
[5]     38.5    0.11  919.58  976570         nmbrCat [5]
              919.21    0.00 2280428/4883242     nmbrCpy [3]
                0.04    0.22  976570/4883645     nmbrTempAlloc [13]
                0.10    0.00 2280428/11109595     nmbrLen [16]
-----------------------------------------------
                0.09  782.29       1/1           command [2]
[6]     32.7    0.09  782.29       1         nmbrUnsquishProof [6]
                0.04  308.19  327287/976570      nmbrCat [5]
                0.09  132.04  327289/976996      nmbrLet [8]
                0.02  132.03  327287/976569      nmbrRight [9]
                0.02  104.87  327287/976570      nmbrLeft [10]
                0.00  104.87  327287/327638      nmbrSeg [12]
                0.13    0.00  327287/329465      nmbrGetSubproofLen [27]
                0.01    0.00       1/2           nmbrMakeTempAlloc [35]
                0.00    0.00       1/11109595     nmbrLen [16]
-----------------------------------------------
              104.90    0.00  327638/1304208     nmbrSeg [12]
              312.65    0.00  976570/1304208     nmbrLeft [10]
[7]     17.5  417.55    0.00 1304208         nmbrNCpy [7]
-----------------------------------------------
                0.00    0.00       1/976996      freeCommandLine [48]
                0.00    0.00       3/976996      nmbrCvtRToVString [47]
                0.00    0.00       5/976996      eraseSource [28]
                0.00    0.00      11/976996      parseCommandLine [43]
                0.00    0.01      19/976996      command [2]
                0.00    0.01      33/976996      compressProof [34]
                0.09  132.04  327289/976996      nmbrUnsquishProof [6]
                0.18  262.08  649635/976996      nmbrSquishProof [4]
[8]     16.5    0.27  394.15  976996         nmbrLet [8]
              393.80    0.00  976954/4883242     nmbrCpy [3]
                0.04    0.22  976996/4883645     nmbrTempAlloc [13]
                0.09    0.00 1953992/11109595     nmbrLen [16]
                0.00    0.00      41/3906950     poolMalloc [15]
                0.00    0.00      39/4492743     poolFree [20]
                0.00    0.00  976996/976996      nmbrAllocLen [67]
                0.00    0.00      23/38          addToUsedPool [89]
-----------------------------------------------
                0.00    0.00       2/976569      compressProof [34]
                0.02  132.03  327287/976569      nmbrUnsquishProof [6]
                0.03  261.92  649280/976569      nmbrSquishProof [4]
[9]     16.5    0.05  393.95  976569         nmbrRight [9]
              393.64    0.00  976568/4883242     nmbrCpy [3]
                0.04    0.22  976568/4883645     nmbrTempAlloc [13]
                0.04    0.00  976569/11109595     nmbrLen [16]
-----------------------------------------------
                0.00    0.00       3/976570      compressProof [34]
                0.02  104.87  327287/976570      nmbrUnsquishProof [6]
                0.03  208.04  649280/976570      nmbrSquishProof [4]
[10]    13.1    0.04  312.92  976570         nmbrLeft [10]
              312.65    0.00  976570/1304208     nmbrNCpy [7]
                0.04    0.22  976570/4883645     nmbrTempAlloc [13]
-----------------------------------------------
                0.00    0.00      11/649291      parseCommandLine [43]
                0.07  261.92  649280/649291      nmbrSquishProof [4]
[11]    11.0    0.07  261.93  649291         nmbrAddElement [11]
              261.72    0.00  649291/4883242     nmbrCpy [3]
                0.03    0.15  649291/4883645     nmbrTempAlloc [13]
                0.03    0.00  649291/11109595     nmbrLen [16]
-----------------------------------------------
                0.00    0.11     351/327638      nmbrSquishProof [4]
                0.00  104.87  327287/327638      nmbrUnsquishProof [6]
[12]     4.4    0.00  104.98  327638         nmbrSeg [12]
              104.90    0.00  327638/1304208     nmbrNCpy [7]
                0.01    0.07  327638/4883645     nmbrTempAlloc [13]
-----------------------------------------------
                0.00    0.00       1/4883645     nmbrUnion [44]
                0.00    0.00      11/4883645     nmbrSpace [54]
                0.01    0.07  327638/4883645     nmbrSeg [12]
                0.03    0.15  649291/4883645     nmbrAddElement [11]
                0.04    0.22  976568/4883645     nmbrRight [9]
                0.04    0.22  976570/4883645     nmbrCat [5]
                0.04    0.22  976570/4883645     nmbrLeft [10]
                0.04    0.22  976996/4883645     nmbrLet [8]
[13]     0.1    0.19    1.12 4883645         nmbrTempAlloc [13]
                0.13    0.46 3906649/3906950     poolMalloc [15]
                0.34    0.00 3906651/4492743     poolFree [20]
                0.18    0.00 3906651/11109595     nmbrLen [16]
-----------------------------------------------
                0.00    0.92       1/1           command [2]
[14]     0.0    0.00    0.92       1         readInput [14]
                0.00    0.47       1/1           readSourceAndIncludes [17]
                0.17    0.05       1/1           parseStatements [22]
                0.14    0.00       1/1           readRawSource [25]
                0.07    0.00       1/1           parseKeywords [30]
                0.01    0.01       1/1           parseLabels [36]
                0.00    0.00       1/1           parseMathDecl [49]
                0.00    0.00       2/86554       let [70]
                0.00    0.00       1/924         cat [77]
-----------------------------------------------
                0.00    0.00      41/3906950     nmbrLet [8]
                0.00    0.00      47/3906950     pntrLet [52]
                0.00    0.00     213/3906950     pntrTempAlloc [50]
                0.13    0.46 3906649/3906950     nmbrTempAlloc [13]
[15]     0.0    0.14    0.46 3906950         poolMalloc [15]
                0.46    0.00 2866827/2866829     memFreePoolPurge [19]
-----------------------------------------------
                0.00    0.00       1/11109595     nmbrCvtRToVString [47]
                0.00    0.00       1/11109595     nmbrUnsquishProof [6]
                0.00    0.00       1/11109595     parseCompressedProof [60]
                0.00    0.00       3/11109595     nmbrUnion [44]
                0.00    0.00       4/11109595     command [2]
                0.00    0.00       4/11109595     nmbrMakeTempAlloc [35]
                0.00    0.00       4/11109595     compressProof [34]
                0.00    0.00     256/11109595     nmbrSquishProof [4]
                0.00    0.00   43638/11109595     parseStatements [22]
                0.03    0.00  649291/11109595     nmbrAddElement [11]
                0.04    0.00  976569/11109595     nmbrRight [9]
                0.06    0.00 1298752/11109595     nmbrInstr [23]
                0.09    0.00 1953992/11109595     nmbrLet [8]
                0.10    0.00 2280428/11109595     nmbrCat [5]
                0.18    0.00 3906651/11109595     nmbrTempAlloc [13]
[16]     0.0    0.51    0.00 11109595         nmbrLen [16]
-----------------------------------------------
                0.00    0.47       1/1           readInput [14]
[17]     0.0    0.00    0.47       1         readSourceAndIncludes [17]
                0.00    0.47       1/1           readInclude [18]
                0.00    0.00       1/93          print2 [61]
                0.00    0.00       5/86554       let [70]
                0.00    0.00       1/924         cat [77]
                0.00    0.00       1/1           readFileToString [109]
-----------------------------------------------
                                  49             readInclude [18]
                0.00    0.47       1/1           readSourceAndIncludes [17]
[18]     0.0    0.00    0.47       1+49      readInclude [18]
                0.06    0.27     109/109         getNextInclusion [21]
                0.14    0.00     118/118         countLines [26]
                0.00    0.00     971/86554       let [70]
                0.00    0.00     157/416         seg [79]
                                  49             readInclude [18]
-----------------------------------------------
                0.00    0.00       1/2866829     eraseSource [28]
                0.00    0.00       1/2866829     freeData [64]
                0.46    0.00 2866827/2866829     poolMalloc [15]
[19]     0.0    0.46    0.00 2866829         memFreePoolPurge [19]
-----------------------------------------------
                0.00    0.00      39/4492743     nmbrLet [8]
                0.00    0.00      47/4492743     pntrLet [52]
                0.00    0.00     213/4492743     pntrTempAlloc [50]
                0.05    0.00  585793/4492743     eraseSource [28]
                0.34    0.00 3906651/4492743     nmbrTempAlloc [13]
[20]     0.0    0.40    0.00 4492743         poolFree [20]
-----------------------------------------------
                0.06    0.27     109/109         readInclude [18]
[21]     0.0    0.06    0.27     109         getNextInclusion [21]
                0.16    0.00 10360745/10360745     rawWhiteSpaceLen [24]
                0.11    0.00 10360745/10360745     rawTokenLen [29]
                0.00    0.00     109/86554       let [70]
                0.00    0.00      59/289         left [81]
-----------------------------------------------
                0.17    0.05       1/1           readInput [14]
[22]     0.0    0.17    0.05       1         parseStatements [22]
                0.03    0.00 2252072/2560291     tokenLen [33]
                0.03    0.00 2252072/2560399     whiteSpaceLen [32]
                0.00    0.00   43638/11109595     nmbrLen [16]
                0.00    0.00  584224/585793      poolFixedMalloc [68]
                0.00    0.00       1/86554       let [70]
-----------------------------------------------
                0.15    0.06  649376/649376      nmbrSquishProof [4]
[23]     0.0    0.15    0.06  649376         nmbrInstr [23]
                0.06    0.00 1298752/11109595     nmbrLen [16]
-----------------------------------------------
                0.16    0.00 10360745/10360745     getNextInclusion [21]
[24]     0.0    0.16    0.00 10360745         rawWhiteSpaceLen [24]
-----------------------------------------------
                0.14    0.00       1/1           readInput [14]
[25]     0.0    0.14    0.00       1         readRawSource [25]
                0.00    0.00       1/93          print2 [61]
-----------------------------------------------
                0.14    0.00     118/118         readInclude [18]
[26]     0.0    0.14    0.00     118         countLines [26]
-----------------------------------------------
                             1153547             nmbrGetSubproofLen [27]
                0.00    0.00    2178/329465      nmbrSquishProof [4]
                0.13    0.00  327287/329465      nmbrUnsquishProof [6]
[27]     0.0    0.13    0.00  329465+1153547 nmbrGetSubproofLen [27]
                             1153547             nmbrGetSubproofLen [27]
-----------------------------------------------
                0.06    0.05       1/1           command [2]
[28]     0.0    0.06    0.05       1         eraseSource [28]
                0.05    0.00  585793/4492743     poolFree [20]
                0.00    0.00       5/976996      nmbrLet [8]
                0.00    0.00       1/2           getContrib [55]
                0.00    0.00       1/2866829     memFreePoolPurge [19]
                0.00    0.00       1/258         pntrLet [52]
                0.00    0.00    2028/86554       let [70]
                0.00    0.00       1/2           eraseTexDefs [101]
                0.00    0.00       1/2           initBigArrays [103]
                0.00    0.00       1/1           getMarkupFlag [108]
-----------------------------------------------
                0.11    0.00 10360745/10360745     getNextInclusion [21]
[29]     0.0    0.11    0.00 10360745         rawTokenLen [29]
-----------------------------------------------
                0.07    0.00       1/1           readInput [14]
[30]     0.0    0.07    0.00       1         parseKeywords [30]
                0.00    0.00       1/93          print2 [61]
-----------------------------------------------
                                                 
[31]     0.0    0.06    0.00                 mathSrchCmp [31]
-----------------------------------------------
                0.00    0.00       1/2560399     parseProof [59]
                0.00    0.00     107/2560399     parseCompressedProof [60]
                0.00    0.00    3234/2560399     parseMathDecl [49]
                0.00    0.00  304985/2560399     parseLabels [36]
                0.03    0.00 2252072/2560399     parseStatements [22]
[32]     0.0    0.03    0.00 2560399         whiteSpaceLen [32]
-----------------------------------------------
                0.00    0.00    3234/2560291     parseMathDecl [49]
                0.00    0.00  304985/2560291     parseLabels [36]
                0.03    0.00 2252072/2560291     parseStatements [22]
[33]     0.0    0.03    0.00 2560291         tokenLen [33]
-----------------------------------------------
                0.00    0.03       1/1           command [2]
[34]     0.0    0.00    0.03       1         compressProof [34]
                0.00    0.01      33/976996      nmbrLet [8]
                0.00    0.01       1/1           nmbrUnion [44]
                0.00    0.00    2178/4462        nmbrElementIn [38]
                0.00    0.00       3/976570      nmbrCat [5]
                0.00    0.00       1/1           nmbrCvtRToVString [47]
                0.00    0.00       3/976570      nmbrLeft [10]
                0.00    0.00       2/976569      nmbrRight [9]
                0.00    0.00      10/11          nmbrSpace [54]
                0.00    0.00       4/11109595     nmbrLen [16]
                0.00    0.00      13/13          knapsack01 [96]
                0.00    0.00      11/86554       let [70]
                0.00    0.00       6/15          space [93]
                0.00    0.00       6/924         cat [77]
                0.00    0.00       2/18          string [91]
                0.00    0.00       1/2           getSourceIndentation [102]
                0.00    0.00       1/289         left [81]
                0.00    0.00       1/2           makeTempAlloc [104]
-----------------------------------------------
                0.01    0.00       1/2           nmbrSquishProof [4]
                0.01    0.00       1/2           nmbrUnsquishProof [6]
[35]     0.0    0.02    0.00       2         nmbrMakeTempAlloc [35]
                0.00    0.00       4/11109595     nmbrLen [16]
-----------------------------------------------
                0.01    0.01       1/1           readInput [14]
[36]     0.0    0.01    0.01       1         parseLabels [36]
                0.00    0.00  304985/2560291     tokenLen [33]
                0.00    0.00  304985/2560399     whiteSpaceLen [32]
-----------------------------------------------
                                                 
[37]     0.0    0.01    0.00                 labelSortCmp [37]
-----------------------------------------------
                0.00    0.00       1/4462        command [2]
                0.00    0.00     105/4462        nmbrCvtRToVString [47]
                0.00    0.00    2178/4462        nmbrUnion [44]
                0.00    0.00    2178/4462        compressProof [34]
[38]     0.0    0.01    0.00    4462         nmbrElementIn [38]
-----------------------------------------------
                                                 
[39]     0.0    0.01    0.00                 free [39]
-----------------------------------------------
                                                 
[40]     0.0    0.01    0.00                 isgraph [40]
-----------------------------------------------
                                                 
[41]     0.0    0.01    0.00                 malloc [41]
-----------------------------------------------
                                                 
[42]     0.0    0.01    0.00                 mathSortCmp [42]
-----------------------------------------------
                0.00    0.01       4/4           command [2]
[43]     0.0    0.00    0.01       4         parseCommandLine [43]
                0.00    0.00      11/976996      nmbrLet [8]
                0.00    0.00      11/649291      nmbrAddElement [11]
                0.00    0.00      11/258         pntrLet [52]
                0.00    0.00      11/191         pntrAddElement [53]
                0.00    0.00     117/124         chr [86]
                0.00    0.00     116/41409       instr [71]
                0.00    0.00      59/171977      freeTempAlloc [69]
                0.00    0.00      15/149         len [84]
                0.00    0.00      11/86554       let [70]
                0.00    0.00      10/416         seg [79]
-----------------------------------------------
                0.00    0.01       1/1           compressProof [34]
[44]     0.0    0.00    0.01       1         nmbrUnion [44]
                0.00    0.00    2178/4462        nmbrElementIn [38]
                0.00    0.00       1/4883242     nmbrCpy [3]
                0.00    0.00       1/4883645     nmbrTempAlloc [13]
                0.00    0.00       3/11109595     nmbrLen [16]
                0.00    0.00     285/287         nmbrZapLen [82]
-----------------------------------------------
                                                 
[45]     0.0    0.01    0.00                 labelSrchCmp [45]
-----------------------------------------------
                                                 
[46]     0.0    0.01    0.00                 nmbrMid [46]
-----------------------------------------------
                0.00    0.00       1/1           compressProof [34]
[47]     0.0    0.00    0.00       1         nmbrCvtRToVString [47]
                0.00    0.00       3/976996      nmbrLet [8]
                0.00    0.00     105/4462        nmbrElementIn [38]
                0.00    0.00       1/11          nmbrSpace [54]
                0.00    0.00       1/11109595     nmbrLen [16]
                0.00    0.00     213/86554       let [70]
                0.00    0.00     105/924         cat [77]
                0.00    0.00       1/15          space [93]
                0.00    0.00       1/289         left [81]
                0.00    0.00       1/2           makeTempAlloc [104]
-----------------------------------------------
                0.00    0.00       1/1           command [2]
[48]     0.0    0.00    0.00       1         freeCommandLine [48]
                0.00    0.00       1/976996      nmbrLet [8]
                0.00    0.00       2/258         pntrLet [52]
                0.00    0.00       3/86554       let [70]
                0.00    0.00       2/1178        pntrLen [76]
-----------------------------------------------
                0.00    0.00       1/1           readInput [14]
[49]     0.0    0.00    0.00       1         parseMathDecl [49]
                0.00    0.00    3234/2560291     tokenLen [33]
                0.00    0.00    3234/2560399     whiteSpaceLen [32]
                0.00    0.00    1568/585793      poolFixedMalloc [68]
                0.00    0.00       1/86554       let [70]
-----------------------------------------------
                0.00    0.00       7/471         pntrSpace [63]
                0.00    0.00      15/471         pntrLeft [57]
                0.00    0.00     191/471         pntrAddElement [53]
                0.00    0.00     258/471         pntrLet [52]
[50]     0.0    0.00    0.00     471         pntrTempAlloc [50]
                0.00    0.00     213/3906950     poolMalloc [15]
                0.00    0.00     213/4492743     poolFree [20]
                0.00    0.00     213/1178        pntrLen [76]
-----------------------------------------------
                                                 
[51]     0.0    0.00    0.00                 getFullArg [51]
                0.00    0.00     198/258         pntrLet [52]
                0.00    0.00     172/191         pntrAddElement [53]
                0.00    0.00      12/15          pntrLeft [57]
                0.00    0.00     618/86554       let [70]
                0.00    0.00     326/924         cat [77]
                0.00    0.00     175/41409       instr [71]
                0.00    0.00     160/416         seg [79]
                0.00    0.00      64/289         left [81]
                0.00    0.00      28/1178        pntrLen [76]
                0.00    0.00       9/11          edit [97]
                0.00    0.00       9/149         len [84]
                0.00    0.00       3/124         chr [86]
-----------------------------------------------
                0.00    0.00       1/258         eraseSource [28]
                0.00    0.00       1/258         freeInOu [65]
                0.00    0.00       2/258         freeCommandLine [48]
                0.00    0.00       4/258         print2 [61]
                0.00    0.00       7/258         processCommandLine [58]
                0.00    0.00       8/258         cmdInput1 [56]
                0.00    0.00      11/258         parseCommandLine [43]
                0.00    0.00      12/258         command [2]
                0.00    0.00      14/258         getContrib [55]
                0.00    0.00     198/258         getFullArg [51]
[52]     0.0    0.00    0.00     258         pntrLet [52]
                0.00    0.00     258/471         pntrTempAlloc [50]
                0.00    0.00      47/3906950     poolMalloc [15]
                0.00    0.00      47/4492743     poolFree [20]
                0.00    0.00     516/1178        pntrLen [76]
                0.00    0.00     258/258         pntrAllocLen [83]
                0.00    0.00     213/404         pntrCpy [80]
                0.00    0.00      15/38          addToUsedPool [89]
-----------------------------------------------
                0.00    0.00       4/191         print2 [61]
                0.00    0.00       4/191         cmdInput1 [56]
                0.00    0.00      11/191         parseCommandLine [43]
                0.00    0.00     172/191         getFullArg [51]
[53]     0.0    0.00    0.00     191         pntrAddElement [53]
                0.00    0.00     191/471         pntrTempAlloc [50]
                0.00    0.00     191/1178        pntrLen [76]
                0.00    0.00     191/404         pntrCpy [80]
-----------------------------------------------
                0.00    0.00       1/11          nmbrCvtRToVString [47]
                0.00    0.00      10/11          compressProof [34]
[54]     0.0    0.00    0.00      11         nmbrSpace [54]
                0.00    0.00      11/4883645     nmbrTempAlloc [13]
-----------------------------------------------
                0.00    0.00       1/2           command [2]
                0.00    0.00       1/2           eraseSource [28]
[55]     0.0    0.00    0.00       2         getContrib [55]
                0.00    0.00      14/258         pntrLet [52]
                0.00    0.00       7/7           pntrSpace [63]
                0.00    0.00      17/86554       let [70]
                0.00    0.00       4/41409       instr [71]
                0.00    0.00       2/416         seg [79]
                0.00    0.00       2/2           compareDates [100]
                0.00    0.00       1/18          string [91]
                0.00    0.00       1/1           getDescription [107]
                0.00    0.00       1/11          edit [97]
                0.00    0.00       1/924         cat [77]
-----------------------------------------------
                0.00    0.00       4/4           command [2]
[56]     0.0    0.00    0.00       4         cmdInput1 [56]
                0.00    0.00       8/258         pntrLet [52]
                0.00    0.00       4/191         pntrAddElement [53]
                0.00    0.00      20/86554       let [70]
                0.00    0.00      11/1178        pntrLen [76]
                0.00    0.00       4/4           cmdInput [99]
                0.00    0.00       4/924         cat [77]
                0.00    0.00       1/289         left [81]
-----------------------------------------------
                0.00    0.00       3/15          processCommandLine [58]
                0.00    0.00      12/15          getFullArg [51]
[57]     0.0    0.00    0.00      15         pntrLeft [57]
                0.00    0.00      15/471         pntrTempAlloc [50]
                0.00    0.00      15/15          pntrNCpy [92]
-----------------------------------------------
                                  14             processCommandLine [58]
                0.00    0.00       4/4           command [2]
[58]     0.0    0.00    0.00       4+14      processCommandLine [58]
                0.00    0.00       7/258         pntrLet [52]
                0.00    0.00       3/15          pntrLeft [57]
                0.00    0.00      74/125         cmdMatches [85]
                0.00    0.00      36/86554       let [70]
                0.00    0.00      33/1178        pntrLen [76]
                0.00    0.00      19/924         cat [77]
                0.00    0.00       9/9           lastArgMatches [98]
                0.00    0.00       4/124         chr [86]
                0.00    0.00       4/86          right [88]
                                  14             processCommandLine [58]
-----------------------------------------------
                0.00    0.00       1/1           command [2]
[59]     0.0    0.00    0.00       1         parseProof [59]
                0.00    0.00       1/1           parseCompressedProof [60]
                0.00    0.00       1/2560399     whiteSpaceLen [32]
-----------------------------------------------
                0.00    0.00       1/1           parseProof [59]
[60]     0.0    0.00    0.00       1         parseCompressedProof [60]
                0.00    0.00     107/2560399     whiteSpaceLen [32]
                0.00    0.00       1/11109595     nmbrLen [16]
                0.00    0.00     106/106         proofTokenLen [87]
                0.00    0.00       2/287         nmbrZapLen [82]
                0.00    0.00       1/585793      poolFixedMalloc [68]
-----------------------------------------------
                0.00    0.00       1/93          readRawSource [25]
                0.00    0.00       1/93          parseKeywords [30]
                0.00    0.00       1/93          readSourceAndIncludes [17]
                0.00    0.00       2/93          main [1]
                0.00    0.00       4/93          command [2]
                0.00    0.00      84/93          printLongLine [62]
[61]     0.0    0.00    0.00      93         print2 [61]
                0.00    0.00       4/258         pntrLet [52]
                0.00    0.00       4/191         pntrAddElement [53]
                0.00    0.00      93/41409       instr [71]
                0.00    0.00      93/924         cat [77]
                0.00    0.00      93/86554       let [70]
                0.00    0.00       1/1178        pntrLen [76]
-----------------------------------------------
                0.00    0.00       2/2           command [2]
[62]     0.0    0.00    0.00       2         printLongLine [62]
                0.00    0.00      84/93          print2 [61]
                0.00    0.00     184/86554       let [70]
                0.00    0.00     163/289         left [81]
                0.00    0.00      84/924         cat [77]
                0.00    0.00      83/41409       instr [71]
                0.00    0.00      82/86          right [88]
-----------------------------------------------
                0.00    0.00       7/7           getContrib [55]
[63]     0.0    0.00    0.00       7         pntrSpace [63]
                0.00    0.00       7/471         pntrTempAlloc [50]
-----------------------------------------------
                0.00    0.00       1/1           command [2]
[64]     0.0    0.00    0.00       1         freeData [64]
                0.00    0.00       1/2866829     memFreePoolPurge [19]
                0.00    0.00       3/86554       let [70]
-----------------------------------------------
                0.00    0.00       1/1           command [2]
[65]     0.0    0.00    0.00       1         freeInOu [65]
                0.00    0.00       1/258         pntrLet [52]
                0.00    0.00       1/1178        pntrLen [76]
                0.00    0.00       1/86554       let [70]
-----------------------------------------------
                0.00    0.00  976996/976996      nmbrLet [8]
[67]     0.0    0.00    0.00  976996         nmbrAllocLen [67]
-----------------------------------------------
                0.00    0.00       1/585793      parseCompressedProof [60]
                0.00    0.00    1568/585793      parseMathDecl [49]
                0.00    0.00  584224/585793      parseStatements [22]
[68]     0.0    0.00    0.00  585793         poolFixedMalloc [68]
-----------------------------------------------
                0.00    0.00       1/171977      str [110]
                0.00    0.00       2/171977      makeTempAlloc [104]
                0.00    0.00      11/171977      edit [97]
                0.00    0.00      18/171977      string [91]
                0.00    0.00      59/171977      parseCommandLine [43]
                0.00    0.00     124/171977      chr [86]
                0.00    0.00     705/171977      mid [78]
                0.00    0.00     924/171977      cat [77]
                0.00    0.00   40898/171977      entry [72]
                0.00    0.00   42681/171977      tempAlloc [432]
                0.00    0.00   86554/171977      let [70]
[69]     0.0    0.00    0.00  171977         freeTempAlloc [69]
-----------------------------------------------
                0.00    0.00       1/86554       main [1]
                0.00    0.00       1/86554       freeInOu [65]
                0.00    0.00       1/86554       parseMathDecl [49]
                0.00    0.00       1/86554       parseStatements [22]
                0.00    0.00       2/86554       readInput [14]
                0.00    0.00       2/86554       getDescription [107]
                0.00    0.00       3/86554       freeCommandLine [48]
                0.00    0.00       3/86554       getMarkupFlag [108]
                0.00    0.00       3/86554       freeData [64]
                0.00    0.00       5/86554       cmdInput [99]
                0.00    0.00       5/86554       readSourceAndIncludes [17]
                0.00    0.00      11/86554       parseCommandLine [43]
                0.00    0.00      11/86554       compressProof [34]
                0.00    0.00      17/86554       getContrib [55]
                0.00    0.00      20/86554       cmdInput1 [56]
                0.00    0.00      36/86554       processCommandLine [58]
                0.00    0.00      56/86554       eraseTexDefs [101]
                0.00    0.00      83/86554       command [2]
                0.00    0.00      93/86554       print2 [61]
                0.00    0.00     109/86554       getNextInclusion [21]
                0.00    0.00     184/86554       printLongLine [62]
                0.00    0.00     213/86554       nmbrCvtRToVString [47]
                0.00    0.00     281/86554       cmdMatches [85]
                0.00    0.00     618/86554       getFullArg [51]
                0.00    0.00     971/86554       readInclude [18]
                0.00    0.00    2028/86554       eraseSource [28]
                0.00    0.00   81796/86554       matchesList [74]
[70]     0.0    0.00    0.00   86554         let [70]
                0.00    0.00   86554/171977      freeTempAlloc [69]
-----------------------------------------------
                0.00    0.00       4/41409       getContrib [55]
                0.00    0.00       4/41409       rinstr [105]
                0.00    0.00      36/41409       switchPos [90]
                0.00    0.00      83/41409       printLongLine [62]
                0.00    0.00      93/41409       print2 [61]
                0.00    0.00     116/41409       parseCommandLine [43]
                0.00    0.00     175/41409       getFullArg [51]
                0.00    0.00   40898/41409       matches [73]
[71]     0.0    0.00    0.00   41409         instr [71]
-----------------------------------------------
                0.00    0.00   40898/40898       matchesList [74]
[72]     0.0    0.00    0.00   40898         entry [72]
                0.00    0.00   40898/171977      freeTempAlloc [69]
-----------------------------------------------
                0.00    0.00   40898/40898       matchesList [74]
[73]     0.0    0.00    0.00   40898         matches [73]
                0.00    0.00   40898/41409       instr [71]
-----------------------------------------------
                0.00    0.00   40898/40898       command [2]
[74]     0.0    0.00    0.00   40898         matchesList [74]
                0.00    0.00   81796/86554       let [70]
                0.00    0.00   40898/40898       numEntries [75]
                0.00    0.00   40898/40898       entry [72]
                0.00    0.00   40898/40898       matches [73]
-----------------------------------------------
                0.00    0.00   40898/40898       matchesList [74]
[75]     0.0    0.00    0.00   40898         numEntries [75]
-----------------------------------------------
                0.00    0.00       1/1178        print2 [61]
                0.00    0.00       1/1178        freeInOu [65]
                0.00    0.00       2/1178        freeCommandLine [48]
                0.00    0.00       9/1178        lastArgMatches [98]
                0.00    0.00      11/1178        cmdInput1 [56]
                0.00    0.00      12/1178        command [2]
                0.00    0.00      28/1178        getFullArg [51]
                0.00    0.00      33/1178        processCommandLine [58]
                0.00    0.00      36/1178        switchPos [90]
                0.00    0.00     125/1178        cmdMatches [85]
                0.00    0.00     191/1178        pntrAddElement [53]
                0.00    0.00     213/1178        pntrTempAlloc [50]
                0.00    0.00     516/1178        pntrLet [52]
[76]     0.0    0.00    0.00    1178         pntrLen [76]
-----------------------------------------------
                0.00    0.00       1/924         readInput [14]
                0.00    0.00       1/924         getContrib [55]
                0.00    0.00       1/924         readSourceAndIncludes [17]
                0.00    0.00       4/924         command [2]
                0.00    0.00       4/924         cmdInput1 [56]
                0.00    0.00       6/924         compressProof [34]
                0.00    0.00      19/924         processCommandLine [58]
                0.00    0.00      84/924         printLongLine [62]
                0.00    0.00      93/924         print2 [61]
                0.00    0.00     105/924         nmbrCvtRToVString [47]
                0.00    0.00     280/924         cmdMatches [85]
                0.00    0.00     326/924         getFullArg [51]
[77]     0.0    0.00    0.00     924         cat [77]
                0.00    0.00     924/171977      freeTempAlloc [69]
-----------------------------------------------
                0.00    0.00     289/705         left [81]
                0.00    0.00     416/705         seg [79]
[78]     0.0    0.00    0.00     705         mid [78]
                0.00    0.00     705/171977      freeTempAlloc [69]
-----------------------------------------------
                0.00    0.00       1/416         getDescription [107]
                0.00    0.00       2/416         getContrib [55]
                0.00    0.00      10/416         parseCommandLine [43]
                0.00    0.00      86/416         right [88]
                0.00    0.00     157/416         readInclude [18]
                0.00    0.00     160/416         getFullArg [51]
[79]     0.0    0.00    0.00     416         seg [79]
                0.00    0.00     416/705         mid [78]
-----------------------------------------------
                0.00    0.00     191/404         pntrAddElement [53]
                0.00    0.00     213/404         pntrLet [52]
[80]     0.0    0.00    0.00     404         pntrCpy [80]
-----------------------------------------------
                0.00    0.00       1/289         nmbrCvtRToVString [47]
                0.00    0.00       1/289         compressProof [34]
                0.00    0.00       1/289         cmdInput1 [56]
                0.00    0.00      59/289         getNextInclusion [21]
                0.00    0.00      64/289         getFullArg [51]
                0.00    0.00     163/289         printLongLine [62]
[81]     0.0    0.00    0.00     289         left [81]
                0.00    0.00     289/705         mid [78]
-----------------------------------------------
                0.00    0.00       2/287         parseCompressedProof [60]
                0.00    0.00     285/287         nmbrUnion [44]
[82]     0.0    0.00    0.00     287         nmbrZapLen [82]
-----------------------------------------------
                0.00    0.00     258/258         pntrLet [52]
[83]     0.0    0.00    0.00     258         pntrAllocLen [83]
-----------------------------------------------
                0.00    0.00       9/149         getFullArg [51]
                0.00    0.00      15/149         parseCommandLine [43]
                0.00    0.00     125/149         cmdMatches [85]
[84]     0.0    0.00    0.00     149         len [84]
-----------------------------------------------
                0.00    0.00      51/125         command [2]
                0.00    0.00      74/125         processCommandLine [58]
[85]     0.0    0.00    0.00     125         cmdMatches [85]
                0.00    0.00     281/86554       let [70]
                0.00    0.00     280/924         cat [77]
                0.00    0.00     125/149         len [84]
                0.00    0.00     125/1178        pntrLen [76]
-----------------------------------------------
                0.00    0.00       3/124         getFullArg [51]
                0.00    0.00       4/124         processCommandLine [58]
                0.00    0.00     117/124         parseCommandLine [43]
[86]     0.0    0.00    0.00     124         chr [86]
                0.00    0.00     124/171977      freeTempAlloc [69]
-----------------------------------------------
                0.00    0.00     106/106         parseCompressedProof [60]
[87]     0.0    0.00    0.00     106         proofTokenLen [87]
-----------------------------------------------
                0.00    0.00       4/86          processCommandLine [58]
                0.00    0.00      82/86          printLongLine [62]
[88]     0.0    0.00    0.00      86         right [88]
                0.00    0.00      86/416         seg [79]
-----------------------------------------------
                0.00    0.00      15/38          pntrLet [52]
                0.00    0.00      23/38          nmbrLet [8]
[89]     0.0    0.00    0.00      38         addToUsedPool [89]
-----------------------------------------------
                0.00    0.00      36/36          command [2]
[90]     0.0    0.00    0.00      36         switchPos [90]
                0.00    0.00      36/41409       instr [71]
                0.00    0.00      36/1178        pntrLen [76]
-----------------------------------------------
                0.00    0.00       1/18          getContrib [55]
                0.00    0.00       2/18          compressProof [34]
                0.00    0.00      15/18          space [93]
[91]     0.0    0.00    0.00      18         string [91]
                0.00    0.00      18/171977      freeTempAlloc [69]
-----------------------------------------------
                0.00    0.00      15/15          pntrLeft [57]
[92]     0.0    0.00    0.00      15         pntrNCpy [92]
-----------------------------------------------
                0.00    0.00       1/15          main [1]
                0.00    0.00       1/15          nmbrCvtRToVString [47]
                0.00    0.00       1/15          getDescription [107]
                0.00    0.00       2/15          command [2]
                0.00    0.00       4/15          cmdInput [99]
                0.00    0.00       6/15          compressProof [34]
[93]     0.0    0.00    0.00      15         space [93]
                0.00    0.00      15/18          string [91]
-----------------------------------------------
                0.00    0.00      13/13          knapsack01 [96]
[94]     0.0    0.00    0.00      13         alloc2DMatrix [94]
-----------------------------------------------
                0.00    0.00      13/13          knapsack01 [96]
[95]     0.0    0.00    0.00      13         free2DMatrix [95]
-----------------------------------------------
                0.00    0.00      13/13          compressProof [34]
[96]     0.0    0.00    0.00      13         knapsack01 [96]
                0.00    0.00      13/13          alloc2DMatrix [94]
                0.00    0.00      13/13          free2DMatrix [95]
-----------------------------------------------
                0.00    0.00       1/11          getDescription [107]
                0.00    0.00       1/11          getContrib [55]
                0.00    0.00       9/11          getFullArg [51]
[97]     0.0    0.00    0.00      11         edit [97]
                0.00    0.00      11/171977      freeTempAlloc [69]
-----------------------------------------------
                0.00    0.00       9/9           processCommandLine [58]
[98]     0.0    0.00    0.00       9         lastArgMatches [98]
                0.00    0.00       9/1178        pntrLen [76]
-----------------------------------------------
                0.00    0.00       4/4           cmdInput1 [56]
[99]     0.0    0.00    0.00       4         cmdInput [99]
                0.00    0.00       5/86554       let [70]
                0.00    0.00       4/15          space [93]
-----------------------------------------------
                0.00    0.00       2/2           getContrib [55]
[100]    0.0    0.00    0.00       2         compareDates [100]
-----------------------------------------------
                0.00    0.00       1/2           command [2]
                0.00    0.00       1/2           eraseSource [28]
[101]    0.0    0.00    0.00       2         eraseTexDefs [101]
                0.00    0.00      56/86554       let [70]
-----------------------------------------------
                0.00    0.00       1/2           command [2]
                0.00    0.00       1/2           compressProof [34]
[102]    0.0    0.00    0.00       2         getSourceIndentation [102]
-----------------------------------------------
                0.00    0.00       1/2           main [1]
                0.00    0.00       1/2           eraseSource [28]
[103]    0.0    0.00    0.00       2         initBigArrays [103]
-----------------------------------------------
                0.00    0.00       1/2           nmbrCvtRToVString [47]
                0.00    0.00       1/2           compressProof [34]
[104]    0.0    0.00    0.00       2         makeTempAlloc [104]
                0.00    0.00       2/171977      freeTempAlloc [69]
-----------------------------------------------
                0.00    0.00       2/2           getDescription [107]
[105]    0.0    0.00    0.00       2         rinstr [105]
                0.00    0.00       4/41409       instr [71]
-----------------------------------------------
                0.00    0.00       1/1           command [2]
[106]    0.0    0.00    0.00       1         fSafeOpen [106]
-----------------------------------------------
                0.00    0.00       1/1           getContrib [55]
[107]    0.0    0.00    0.00       1         getDescription [107]
                0.00    0.00       2/86554       let [70]
                0.00    0.00       2/2           rinstr [105]
                0.00    0.00       1/15          space [93]
                0.00    0.00       1/416         seg [79]
                0.00    0.00       1/11          edit [97]
-----------------------------------------------
                0.00    0.00       1/1           eraseSource [28]
[108]    0.0    0.00    0.00       1         getMarkupFlag [108]
                0.00    0.00       3/86554       let [70]
-----------------------------------------------
                0.00    0.00       1/1           readSourceAndIncludes [17]
[109]    0.0    0.00    0.00       1         readFileToString [109]
-----------------------------------------------
                0.00    0.00       1/1           command [2]
[110]    0.0    0.00    0.00       1         str [110]
                0.00    0.00       1/171977      freeTempAlloc [69]
-----------------------------------------------

 This table describes the call tree of the program, and was sorted by
 the total amount of time spent in each function and its children.

 Each entry in this table consists of several lines.  The line with the
 index number at the left hand margin lists the current function.
 The lines above it list the functions that called this function,
 and the lines below it list the functions this one called.
 This line lists:
     index      A unique number given to each element of the table.
                Index numbers are sorted numerically.
                The index number is printed next to every function name so
                it is easier to look up where the function is in the table.

     % time     This is the percentage of the `total' time that was spent
                in this function and its children.  Note that due to
                different viewpoints, functions excluded by options, etc,
                these numbers will NOT add up to 100%.

     self       This is the total amount of time spent in this function.

     children   This is the total amount of time propagated into this
                function by its children.

     called     This is the number of times the function was called.
                If the function called itself recursively, the number
                only includes non-recursive calls, and is followed by
                a `+' and the number of recursive calls.

     name       The name of the current function.  The index number is
                printed after it.  If the function is a member of a
                cycle, the cycle number is printed between the
                function's name and the index number.

 For the function's parents, the fields have the following meanings:

     self       This is the amount of time that was propagated directly
                from the function into this parent.

     children   This is the amount of time that was propagated from
                the function's children into this parent.

     called     This is the number of times this parent called the
                function `/' the total number of times the function
                was called.  Recursive calls to the function are not
                included in the number after the `/'.

     name       This is the name of the parent.  The parent's index
                number is printed after it.  If the parent is a
                member of a cycle, the cycle number is printed between
                the name and the index number.

 If the parents of the function cannot be determined, the word
 `' is printed in the `name' field, and all the other
 fields are blank.

 For the function's children, the fields have the following meanings:

     self       This is the amount of time that was propagated directly
                from the child into the function.

     children   This is the amount of time that was propagated from the
                child's children to the function.

     called     This is the number of times the function called
                this child `/' the total number of times the child
                was called.  Recursive calls by the child are not
                listed in the number after the `/'.

     name       This is the name of the child.  The child's index
                number is printed after it.  If the child is a
                member of a cycle, the cycle number is printed
                between the name and the index number.

 If there are any cycles (circles) in the call graph, there is an
 entry for the cycle-as-a-whole.  This entry shows who called the
 cycle (as parents) and the members of the cycle (as children.)
 The `+' recursive calls entry shows the number of function calls that
 were internal to the cycle, and the calls entry for each member shows,
 for that member, how many times it was called from other members of
 the cycle.
♀
Copyright (C) 2012-2017 Free Software Foundation, Inc.

Copying and distribution of this file, with or without modification,
are permitted in any medium without royalty provided the copyright
notice and this notice are preserved.
♀
Index by function name

  [89] addToUsedPool          [70] let                    [49] parseMathDecl
  [94] alloc2DMatrix         [104] makeTempAlloc          [59] parseProof
  [77] cat                    [41] malloc                 [22] parseStatements
  [86] chr                    [73] matches                [53] pntrAddElement
  [99] cmdInput               [74] matchesList            [83] pntrAllocLen
  [56] cmdInput1              [42] mathSortCmp            [80] pntrCpy
  [85] cmdMatches             [31] mathSrchCmp            [57] pntrLeft
   [2] command                [19] memFreePoolPurge       [76] pntrLen
 [100] compareDates           [78] mid                    [52] pntrLet
  [34] compressProof          [11] nmbrAddElement         [92] pntrNCpy
  [26] countLines             [67] nmbrAllocLen           [63] pntrSpace
  [97] edit                    [5] nmbrCat                [50] pntrTempAlloc
  [72] entry                   [3] nmbrCpy                [68] poolFixedMalloc
  [28] eraseSource            [47] nmbrCvtRToVString      [20] poolFree
 [101] eraseTexDefs           [38] nmbrElementIn          [15] poolMalloc
 [106] fSafeOpen              [27] nmbrGetSubproofLen     [61] print2
  [39] free                   [23] nmbrInstr              [62] printLongLine
  [95] free2DMatrix           [10] nmbrLeft               [58] processCommandLine
  [48] freeCommandLine        [16] nmbrLen                [87] proofTokenLen
  [64] freeData                [8] nmbrLet                [29] rawTokenLen
  [65] freeInOu               [35] nmbrMakeTempAlloc      [24] rawWhiteSpaceLen
  [69] freeTempAlloc          [46] nmbrMid               [109] readFileToString
  [55] getContrib              [7] nmbrNCpy               [18] readInclude
 [107] getDescription          [9] nmbrRight              [14] readInput
 [108] getMarkupFlag          [12] nmbrSeg                [25] readRawSource
  [21] getNextInclusion       [54] nmbrSpace              [17] readSourceAndIncludes
 [102] getSourceIndentation    [4] nmbrSquishProof        [88] right
 [103] initBigArrays          [13] nmbrTempAlloc         [105] rinstr
  [71] instr                  [44] nmbrUnion              [79] seg
  [40] isgraph                 [6] nmbrUnsquishProof      [93] space
  [96] knapsack01             [82] nmbrZapLen            [110] str
  [37] labelSortCmp           [75] numEntries             [91] string
  [45] labelSrchCmp           [43] parseCommandLine       [90] switchPos
  [98] lastArgMatches         [60] parseCompressedProof   [33] tokenLen
  [81] left                   [30] parseKeywords          [32] whiteSpaceLen
  [84] len                    [36] parseLabels

tirix commented 1 year ago

I propose to open a new issue in metamath-exe to track a possible issue with the program. This issue should be closed as soon as #3275 is merged, since the split version of ~ footex can be minimized efficiently.

GinoGiotto commented 1 year ago

I propose to open a new issue in metamath-exe to track a possible issue with the program. This issue should be closed as soon as #3275 is merged, since the split version of ~ footex can be minimized efficiently.

LGTM, I'll close this as soon as #3275 is merged.

metamath / set.mm

Footex needs revision #3271