ghost
commented
10 years ago Bad link. Here it is again: The file Lib.thy fails to process in Lib.thy.
Closed ghost closed 9 years ago
ghost
commented
10 years ago Bad link. Here it is again: The file Lib.thy fails to process in Lib.thy.
phlegmaticprogrammer
commented
10 years ago I ran it, and although it took way too long to be bearable, it at least finished processing on my machine (beautiful Macbook Pro 17inch, 16GB RAM):
run scripts/root.thy /Users/stevenobua/myrepos/proofpeer-hollight/proofscript
[info] Running proofpeer.proofscript.naiveinterpreter.Interpreter scripts/root.thy /Users/stevenobua/myrepos/proofpeer-hollight/proofscript
processing theory file: scripts/root.thy
added theory: \root
processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Big_int.thy
added theory: \Big_int
processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Format.thy
added theory: \Format
processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Lib.thy
added theory: \Lib
processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Num.thy
added theory: \Num
processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Pervasives.thy
added theory: \Pervasives
processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Ratio.thy
added theory: \Ratio
processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/String.thy
added theory: \String
processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Support.thy
added theory: \Support
------------------------------------------------------------
executing theory \root ...
successfully executed theory \root
executing theory \Support ...
successfully executed theory \Support
executing theory \Pervasives ...
successfully executed theory \Pervasives
executing theory \Format ...
successfully executed theory \Format
executing theory \Ratio ...
successfully executed theory \Ratio
executing theory \String ...
successfully executed theory \String
executing theory \Num ...
** show (\Num:64): [true, "", [0, []], ["Ratio", 10, 20]]
** show (\Num:65): true
successfully executed theory \Num
executing theory \Big_int ...
successfully executed theory \Big_int
executing theory \Lib ...
failed executing theory \Lib: function has unknown free variables: applyd
in /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Lib.thy at row 4, column 42
in /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Lib.thy at row 4, column 37
in /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Lib.thy at row 4, column 1
------------------------------------------------------------
Processed 9 theories:
8 theories executed successfully
0 theories failed during preprocessing
1 theories failed during execution
0 theories were skipped because of failed/skipped parent theoriesThis is the Java version which is default on my machine (and I think is used by Scala):
> java -version
java version "1.7.0_45"
Java(TM) SE Runtime Environment (build 1.7.0_45-b18)
Java HotSpot(TM) 64-Bit Server VM (build 24.45-b08, mixed mode)I am going to examine workarounds for now how to speed up the processing phase. I was planning to do this later together with the interactivity and extensible syntax work package, but I can see how you cannot really work at this point properly with such long processing times.
If I manage to speed up processing, then this might also make working on caching etc. for now unnecessary.
phlegmaticprogrammer
commented
10 years ago I've added measurement of parsing times to the interpreter (8b2d6bf7d86bf6f9a00f6a2db1734344e306afcf):
processing theory file: scripts/root.thy
parsed in 3258ms
added theory: \root
processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Big_int.thy
parsed in 331ms
added theory: \Big_int
processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Format.thy
parsed in 177ms
added theory: \Format
processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Lib.thy
parsed in 232862ms
added theory: \Lib
processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Num.thy
parsed in 4747ms
added theory: \Num
processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Pervasives.thy
parsed in 3713ms
added theory: \Pervasives
processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Ratio.thy
parsed in 987ms
added theory: \Ratio
processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/String.thy
parsed in 511ms
added theory: \String
processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Support.thy
parsed in 3611ms
added theory: \SupportIn that case, it might be an issue with a default heap limit on the DICE versions of Java. I'm just glad the monstrosity compiles!
On 18/09/14 22:18, Steven Obua wrote:
I ran it, and although it took way too long to be bearable, it at least finished processing on my machine (beautiful Macbook Pro 17inch, 16GB RAM):
run scripts/root.thy /Users/stevenobua/myrepos/proofpeer-hollight/proofscript [info] Running proofpeer.proofscript.naiveinterpreter.Interpreter scripts/root.thy /Users/stevenobua/myrepos/proofpeer-hollight/proofscript processing theory file: scripts/root.thy added theory: \root processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Big_int.thy added theory: \Big_int processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Format.thy added theory: \Format processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Lib.thy added theory: \Lib processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Num.thy added theory: \Num processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Pervasives.thy added theory: \Pervasives processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Ratio.thy added theory: \Ratio processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/String.thy added theory: \String processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Support.thy added theory: \Support|------------------------------------------------------------
executing theory \root ... successfully executed theory \root executing theory \Support ... successfully executed theory \Support executing theory \Pervasives ... successfully executed theory \Pervasives executing theory \Format ... successfully executed theory \Format executing theory \Ratio ... successfully executed theory \Ratio executing theory \String ... successfully executed theory \String executing theory \Num ... * show (\Num:64): [true, "", [0, []], ["Ratio", 10, 20]] * show (\Num:65): true successfully executed theory \Num executing theory \Big_int ... successfully executed theory \Big_int executing theory \Lib ... failed executing theory \Lib: function has unknown free variables: applyd in /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Lib.thy at row 4, column 42 in /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Lib.thy at row 4, column 37 in /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Lib.thy at row 4, column 1
Processed 9 theories: 8 theories executed successfully 0 theories failed during preprocessing 1 theories failed during execution 0 theories were skipped because of failed/skipped parent theories |
— Reply to this email directly or view it on GitHub https://github.com/proofpeer/proofpeer-proofscript/issues/33#issuecomment-56104757.
phlegmaticprogrammer
commented
10 years ago Just for the record, here are the current parsing times for all theories in the scripts directory:
processing theory file: scripts/bootstrap/classical.thy
parsed in 2005ms
added theory: \Classical
processing theory file: scripts/bootstrap/conversions.thy
parsed in 11263ms
added theory: \Conversions
processing theory file: scripts/bootstrap/equal.thy
parsed in 3073ms
added theory: \Equal
processing theory file: scripts/bootstrap/list.thy
parsed in 656ms
added theory: \List
processing theory file: scripts/bootstrap/redundancies.thy
parsed in 5833ms
added theory: \Redundancies
processing theory file: scripts/bootstrap/syntax.thy
parsed in 732ms
added theory: \Syntax
processing theory file: scripts/examples/Blocks.thy
parsed in 3541ms
added theory: \examples\Blocks
processing theory file: scripts/examples/DataTypes.thy
parsed in 13529ms
added theory: \examples\DataTypes
processing theory file: scripts/examples/FunctionsAndContexts.thy
parsed in 2215ms
added theory: \examples\FunctionsAndContexts
processing theory file: scripts/examples/HelloWorld.thy
parsed in 60ms
added theory: \examples\HelloWorld
processing theory file: scripts/examples/Lnamespaces/LA.thy
parsed in 1439ms
added theory: \LA
processing theory file: scripts/examples/Lnamespaces/LB.thy
parsed in 294ms
added theory: \LB
processing theory file: scripts/examples/Lnamespaces/LC.thy
parsed in 421ms
added theory: \LC
processing theory file: scripts/examples/Lnamespaces/LD.thy
parsed in 268ms
added theory: \LD
processing theory file: scripts/examples/Lnamespaces/LE.thy
parsed in 261ms
added theory: \LE
processing theory file: scripts/examples/Lnamespaces/LU.thy
parsed in 50ms
added theory: \examples\namespaces\LU
processing theory file: scripts/examples/Lnamespaces/LV.thy
parsed in 156ms
added theory: \examples\namespaces\LV
processing theory file: scripts/examples/Lnamespaces/LW.thy
parsed in 341ms
added theory: \examples\LW
processing theory file: scripts/examples/Logic.thy
parsed in 9990ms
added theory: \examples\Logic
processing theory file: scripts/examples/LogicStatements.thy
parsed in 5527ms
added theory: \examples\LogicStatements
processing theory file: scripts/examples/namespaces/A.thy
parsed in 164ms
added theory: \A
processing theory file: scripts/examples/namespaces/B.thy
parsed in 262ms
added theory: \B
processing theory file: scripts/examples/namespaces/C.thy
parsed in 410ms
added theory: \C
processing theory file: scripts/examples/namespaces/D.thy
parsed in 387ms
added theory: \D
processing theory file: scripts/examples/namespaces/E.thy
parsed in 775ms
added theory: \E
processing theory file: scripts/examples/namespaces/U.thy
parsed in 80ms
added theory: \examples\namespaces\U
processing theory file: scripts/examples/namespaces/V.thy
parsed in 177ms
added theory: \examples\namespaces\V
processing theory file: scripts/examples/namespaces/W.thy
parsed in 300ms
added theory: \examples\W
processing theory file: scripts/examples/Naming.thy
parsed in 1455ms
added theory: \examples\Naming
processing theory file: scripts/examples/Patterns.thy
parsed in 9980ms
added theory: \examples\Patterns
processing theory file: scripts/examples/Statements.thy
parsed in 14292ms
added theory: \examples\Statements
processing theory file: scripts/issues/issue22.thy
parsed in 88ms
added theory: \issue22
processing theory file: scripts/issues/issue24.thy
parsed in 88ms
added theory: \issue24
processing theory file: scripts/issues/issue25.thy
parsed in 287ms
added theory: \issue25
processing theory file: scripts/issues/issue26.thy
parsed in 393ms
added theory: \issue26
processing theory file: scripts/issues/issue27_A.thy
parsed in 273ms
added theory: \issue27_A
processing theory file: scripts/issues/issue27_B.thy
parsed in 1298ms
added theory: \issue27_B
processing theory file: scripts/issues/issue28.thy
parsed in 791ms
added theory: \issue28
processing theory file: scripts/issues/issue29.thy
parsed in 170ms
added theory: \issue29
processing theory file: scripts/issues/issue30.thy
parsed in 1049ms
added theory: \issue30
processing theory file: scripts/issues/issue31.thy
parsed in 1450ms
added theory: \issue31
processing theory file: scripts/issues/issue34.thy
parsed in 392ms
added theory: \issue34
processing theory file: scripts/issues/issue35.thy
parsed in 6197ms
added theory: \issue35
processing theory file: scripts/issues/issue37.thy
parsed in 607ms
added theory: \issue37
processing theory file: scripts/root.thy
parsed in 2042ms
added theory: \rootI tested what kind of speedup one gets by dividing the toplevel into chunks based on indentation at first, and then doing the parsing for each of the chunks separately. The sad answer is that the speedup is negligible (238s instead of 249 seconds for Lib.thy, and 10.3 seconds instead of 11.5 seconds for conversions.thy). The good answer is that the algorithm is already very good out of the box in that it uses the layout constraints very effectively.
So what I have to do now is to see how to optimise the algorithm itself by cutting down the constant factor. That's going to take a while I think (at least a week, I guess), so don't hold your breath.
phlegmaticprogrammer
commented
9 years ago I've made substantial speed improvements by redesigning the parsing algorithm + using custom datastructures instead of the standard Scala ones. To compile, you need to check our the proofpeer-general repository instead of the proofpeer-scala one, by the way.
phlegmaticprogrammer
commented
9 years ago Here are the new parsing times I get:
> run scripts /Users/stevenobua/myrepos/proofpeer-hollight/proofscript
[info] Running proofpeer.proofscript.naiveinterpreter.Interpreter scripts /Users/stevenobua/myrepos/proofpeer-hollight/proofscript
processing theory file: scripts/bootstrap/classical.thy
Initializing parser ...
Parser is initialized.
parsed in 797ms
added theory: \Classical
processing theory file: scripts/bootstrap/connectives.thy
parsed in 290ms
added theory: \Connectives
processing theory file: scripts/bootstrap/conversions.thy
parsed in 118ms
added theory: \Conversions
processing theory file: scripts/bootstrap/equal.thy
parsed in 32ms
added theory: \Equal
processing theory file: scripts/bootstrap/list.thy
parsed in 17ms
added theory: \List
processing theory file: scripts/bootstrap/redundancies.thy
parsed in 13ms
added theory: \Redundancies
processing theory file: scripts/bootstrap/syntax.thy
parsed in 7ms
added theory: \Syntax
processing theory file: scripts/examples/Blocks.thy
parsed in 29ms
added theory: \examples\Blocks
processing theory file: scripts/examples/DataTypes.thy
parsed in 87ms
added theory: \examples\DataTypes
processing theory file: scripts/examples/FunctionsAndContexts.thy
parsed in 21ms
added theory: \examples\FunctionsAndContexts
processing theory file: scripts/examples/HelloWorld.thy
parsed in 1ms
added theory: \examples\HelloWorld
processing theory file: scripts/examples/Lnamespaces/LA.thy
parsed in 8ms
added theory: \LA
processing theory file: scripts/examples/Lnamespaces/LB.thy
parsed in 3ms
added theory: \LB
processing theory file: scripts/examples/Lnamespaces/LC.thy
parsed in 5ms
added theory: \LC
processing theory file: scripts/examples/Lnamespaces/LD.thy
parsed in 4ms
added theory: \LD
processing theory file: scripts/examples/Lnamespaces/LE.thy
parsed in 3ms
added theory: \LE
processing theory file: scripts/examples/Lnamespaces/LU.thy
parsed in 1ms
added theory: \examples\namespaces\LU
processing theory file: scripts/examples/Lnamespaces/LV.thy
parsed in 2ms
added theory: \examples\namespaces\LV
processing theory file: scripts/examples/Lnamespaces/LW.thy
parsed in 4ms
added theory: \examples\LW
processing theory file: scripts/examples/Logic.thy
parsed in 82ms
added theory: \examples\Logic
processing theory file: scripts/examples/LogicStatements.thy
parsed in 53ms
added theory: \examples\LogicStatements
processing theory file: scripts/examples/namespaces/A.thy
parsed in 2ms
added theory: \A
processing theory file: scripts/examples/namespaces/B.thy
parsed in 2ms
added theory: \B
processing theory file: scripts/examples/namespaces/C.thy
parsed in 6ms
added theory: \C
processing theory file: scripts/examples/namespaces/D.thy
parsed in 4ms
added theory: \D
processing theory file: scripts/examples/namespaces/E.thy
parsed in 7ms
added theory: \E
processing theory file: scripts/examples/namespaces/U.thy
parsed in 1ms
added theory: \examples\namespaces\U
processing theory file: scripts/examples/namespaces/V.thy
parsed in 2ms
added theory: \examples\namespaces\V
processing theory file: scripts/examples/namespaces/W.thy
parsed in 2ms
added theory: \examples\W
processing theory file: scripts/examples/Naming.thy
parsed in 9ms
added theory: \examples\Naming
processing theory file: scripts/examples/Patterns.thy
parsed in 67ms
added theory: \examples\Patterns
processing theory file: scripts/examples/Statements.thy
parsed in 75ms
added theory: \examples\Statements
processing theory file: scripts/issues/issue22.thy
parsed in 1ms
added theory: \issue22
processing theory file: scripts/issues/issue24.thy
parsed in 1ms
added theory: \issue24
processing theory file: scripts/issues/issue25.thy
parsed in 3ms
added theory: \issue25
processing theory file: scripts/issues/issue26.thy
parsed in 3ms
added theory: \issue26
processing theory file: scripts/issues/issue27_A.thy
parsed in 2ms
added theory: \issue27_A
processing theory file: scripts/issues/issue27_B.thy
parsed in 8ms
added theory: \issue27_B
processing theory file: scripts/issues/issue28.thy
parsed in 8ms
added theory: \issue28
processing theory file: scripts/issues/issue29.thy
parsed in 2ms
added theory: \issue29
processing theory file: scripts/issues/issue30.thy
parsed in 10ms
added theory: \issue30
processing theory file: scripts/issues/issue31.thy
parsed in 7ms
added theory: \issue31
processing theory file: scripts/issues/issue34.thy
parsed in 3ms
added theory: \issue34
processing theory file: scripts/issues/issue35.thy
parsed in 34ms
added theory: \issue35
processing theory file: scripts/issues/issue37.thy
parsed in 4ms
added theory: \issue37
processing theory file: scripts/root.thy
parsed in 35ms
added theory: \root
processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Big_int.thy
parsed in 4ms
added theory: \Big_int
processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Format.thy
parsed in 3ms
added theory: \Format
processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Lib.thy
parsed in 1732ms
added theory: \Lib
processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Num.thy
parsed in 43ms
added theory: \Num
processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Pervasives.thy
parsed in 21ms
added theory: \Pervasives
processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Ratio.thy
parsed in 12ms
added theory: \Ratio
processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/String.thy
parsed in 3ms
added theory: \String
processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Support.thy
parsed in 20ms
added theory: \Support
------------------------------------------------------------Great work, man! I can get back to my proofscripting now. :)
On 30/09/14 00:02, Steven Obua wrote:
Here are the new parsing times I get:
|> run scripts /Users/stevenobua/myrepos/proofpeer-hollight/proofscript [info] Running proofpeer.proofscript.naiveinterpreter.Interpreter scripts /Users/stevenobua/myrepos/proofpeer-hollight/proofscript processing theory file: scripts/bootstrap/classical.thy Initializing parser ... Parser is initialized. parsed in 797ms added theory: \Classical processing theory file: scripts/bootstrap/connectives.thy parsed in 290ms added theory: \Connectives processing theory file: scripts/bootstrap/conversions.thy parsed in 118ms added theory: \Conversions processing theory file: scripts/bootstrap/equal.thy parsed in 32ms added theory: \Equal processing theory file: scripts/bootstrap/list.thy parsed in 17ms added theory: \List processing theory file: scripts/bootstrap/redundancies.thy parsed in 13ms added theory: \Redundancies processing theory file: scripts/bootstrap/syntax.thy parsed in 7ms added theory: \Syntax processing theory file: scripts/examples/Blocks.thy parsed in 29ms added theory: \examples\Blocks processing theory file: scripts/examples/DataTypes.thy parsed in 87ms added theory: \examples\DataTypes processing theory file: scripts/examples/FunctionsAndContexts.thy parsed in 21ms added theory: \examples\FunctionsAndContexts processing theory file: scripts/examples/HelloWorld.thy parsed in 1ms added theory: \examples\HelloWorld processing theory file: scripts/examples/Lnamespaces/LA.thy parsed in 8ms added theory: \LA processing theory file: scripts/examples/Lnamespaces/LB.thy parsed in 3ms added theory: \LB processing theory file: scripts/examples/Lnamespaces/LC.thy parsed in 5ms added theory: \LC processing theory file: scripts/examples/Lnamespaces/LD.thy parsed in 4ms added theory: \LD processing theory file: scripts/examples/Lnamespaces/LE.thy parsed in 3ms added theory: \LE processing theory file: scripts/examples/Lnamespaces/LU.thy parsed in 1ms added theory: \examples\namespaces\LU processing theory file: scripts/examples/Lnamespaces/LV.thy parsed in 2ms added theory: \examples\namespaces\LV processing theory file: scripts/examples/Lnamespaces/LW.thy parsed in 4ms added theory: \examples\LW processing theory file: scripts/examples/Logic.thy parsed in 82ms added theory: \examples\Logic processing theory file: scripts/examples/LogicStatements.thy parsed in 53ms added theory: \examples\LogicStatements processing theory file: scripts/examples/namespaces/A.thy parsed in 2ms added theory: \A processing theory file: scripts/examples/namespaces/B.thy parsed in 2ms added theory: \B processing theory file: scripts/examples/namespaces/C.thy parsed in 6ms added theory: \C processing theory file: scripts/examples/namespaces/D.thy parsed in 4ms added theory: \D processing theory file: scripts/examples/namespaces/E.thy parsed in 7ms added theory: \E processing theory file: scripts/examples/namespaces/U.thy parsed in 1ms added theory: \examples\namespaces\U processing theory file: scripts/examples/namespaces/V.thy parsed in 2ms added theory: \examples\namespaces\V processing theory file: scripts/examples/namespaces/W.thy parsed in 2ms added theory: \examples\W processing theory file: scripts/examples/Naming.thy parsed in 9ms added theory: \examples\Naming processing theory file: scripts/examples/Patterns.thy parsed in 67ms added theory: \examples\Patterns processing theory file: scripts/examples/Statements.thy parsed in 75ms added theory: \examples\Statements processing theory file: scripts/issues/issue22.thy parsed in 1ms added theory: \issue22 processing theory file: scripts/issues/issue24.thy parsed in 1ms added theory: \issue24 processing theory file: scripts/issues/issue25.thy parsed in 3ms added theory: \issue25 processing theory file: scripts/issues/issue26.thy parsed in 3ms added theory: \issue26 processing theory file: scripts/issues/issue27_A.thy parsed in 2ms added theory: \issue27_A processing theory file: scripts/issues/issue27_B.thy parsed in 8ms added theory: \issue27_B processing theory file: scripts/issues/issue28.thy parsed in 8ms added theory: \issue28 processing theory file: scripts/issues/issue29.thy parsed in 2ms added theory: \issue29 processing theory file: scripts/issues/issue30.thy parsed in 10ms added theory: \issue30 processing theory file: scripts/issues/issue31.thy parsed in 7ms added theory: \issue31 processing theory file: scripts/issues/issue34.thy parsed in 3ms added theory: \issue34 processing theory file: scripts/issues/issue35.thy parsed in 34ms added theory: \issue35 processing theory file: scripts/issues/issue37.thy parsed in 4ms added theory: \issue37 processing theory file: scripts/root.thy parsed in 35ms added theory: \root processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Big_int.thy parsed in 4ms added theory: \Big_int processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Format.thy parsed in 3ms added theory: \Format processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Lib.thy parsed in 1732ms added theory: \Lib processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Num.thy parsed in 43ms added theory: \Num processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Pervasives.thy parsed in 21ms added theory: \Pervasives processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Ratio.thy parsed in 12ms added theory: \Ratio processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/String.thy parsed in 3ms added theory: \String processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Support.thy parsed in 20ms added theory: \Support
— Reply to this email directly or view it on GitHub https://github.com/proofpeer/proofpeer-proofscript/issues/33#issuecomment-57243701.
pikan
commented
9 years ago I concur. Excellent stuff. Things look viable again.
Sent from my iPhone
On 30 Sep 2014, at 12:16, Phil Scott notifications@github.com wrote:
Great work, man! I can get back to my proofscripting now. :)
On 30/09/14 00:02, Steven Obua wrote:
Here are the new parsing times I get:
|> run scripts /Users/stevenobua/myrepos/proofpeer-hollight/proofscript [info] Running proofpeer.proofscript.naiveinterpreter.Interpreter scripts /Users/stevenobua/myrepos/proofpeer-hollight/proofscript processing theory file: scripts/bootstrap/classical.thy Initializing parser ... Parser is initialized. parsed in 797ms added theory: \Classical processing theory file: scripts/bootstrap/connectives.thy parsed in 290ms added theory: \Connectives processing theory file: scripts/bootstrap/conversions.thy parsed in 118ms added theory: \Conversions processing theory file: scripts/bootstrap/equal.thy parsed in 32ms added theory: \Equal processing theory file: scripts/bootstrap/list.thy parsed in 17ms added theory: \List processing theory file: scripts/bootstrap/redundancies.thy parsed in 13ms added theory: \Redundancies processing theory file: scripts/bootstrap/syntax.thy parsed in 7ms added theory: \Syntax processing theory file: scripts/examples/Blocks.thy parsed in 29ms added theory: \examples\Blocks processing theory file: scripts/examples/DataTypes.thy parsed in 87ms added theory: \examples\DataTypes processing theory file: scripts/examples/FunctionsAndContexts.thy parsed in 21ms added theory: \examples\FunctionsAndContexts processing theory file: scripts/examples/HelloWorld.thy parsed in 1ms added theory: \examples\HelloWorld processing theory file: scripts/examples/Lnamespaces/LA.thy parsed in 8ms added theory: \LA processing theory file: scripts/examples/Lnamespaces/LB.thy parsed in 3ms added theory: \LB processing theory file: scripts/examples/Lnamespaces/LC.thy parsed in 5ms added theory: \LC processing theory file: scripts/examples/Lnamespaces/LD.thy parsed in 4ms added theory: \LD processing theory file: scripts/examples/Lnamespaces/LE.thy parsed in 3ms added theory: \LE processing theory file: scripts/examples/Lnamespaces/LU.thy parsed in 1ms added theory: \examples\namespaces\LU processing theory file: scripts/examples/Lnamespaces/LV.thy parsed in 2ms added theory: \examples\namespaces\LV processing theory file: scripts/examples/Lnamespaces/LW.thy parsed in 4ms added theory: \examples\LW processing theory file: scripts/examples/Logic.thy parsed in 82ms added theory: \examples\Logic processing theory file: scripts/examples/LogicStatements.thy parsed in 53ms added theory: \examples\LogicStatements processing theory file: scripts/examples/namespaces/A.thy parsed in 2ms added theory: \A processing theory file: scripts/examples/namespaces/B.thy parsed in 2ms added theory: \B processing theory file: scripts/examples/namespaces/C.thy parsed in 6ms added theory: \C processing theory file: scripts/examples/namespaces/D.thy parsed in 4ms added theory: \D processing theory file: scripts/examples/namespaces/E.thy parsed in 7ms added theory: \E processing theory file: scripts/examples/namespaces/U.thy parsed in 1ms added theory: \examples\namespaces\U processing theory file: scripts/examples/namespaces/V.thy parsed in 2ms added theory: \examples\namespaces\V processing theory file: scripts/examples/namespaces/W.thy parsed in 2ms added theory: \examples\W processing theory file: scripts/examples/Naming.thy parsed in 9ms added theory: \examples\Naming processing theory file: scripts/examples/Patterns.thy parsed in 67ms added theory: \examples\Patterns processing theory file: scripts/examples/Statements.thy parsed in 75ms added theory: \examples\Statements processing theory file: scripts/issues/issue22.thy parsed in 1ms added theory: \issue22 processing theory file: scripts/issues/issue24.thy parsed in 1ms added theory: \issue24 processing theory file: scripts/issues/issue25.thy parsed in 3ms added theory: \issue25 processing theory file: scripts/issues/issue26.thy parsed in 3ms added theory: \issue26 processing theory file: scripts/issues/issue27_A.thy parsed in 2ms added theory: \issue27_A processing theory file: scripts/issues/issue27_B.thy parsed in 8ms added theory: \issue27_B processing theory file: scripts/issues/issue28.thy parsed in 8ms added theory: \issue28 processing theory file: scripts/issues/issue29.thy parsed in 2ms added theory: \issue29 processing theory file: scripts/issues/issue30.thy parsed in 10ms added theory: \issue30 processing theory file: scripts/issues/issue31.thy parsed in 7ms added theory: \issue31 processing theory file: scripts/issues/issue34.thy parsed in 3ms added theory: \issue34 processing theory file: scripts/issues/issue35.thy parsed in 34ms added theory: \issue35 processing theory file: scripts/issues/issue37.thy parsed in 4ms added theory: \issue37 processing theory file: scripts/root.thy parsed in 35ms added theory: \root processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Big_int.thy parsed in 4ms added theory: \Big_int processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Format.thy parsed in 3ms added theory: \Format processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Lib.thy parsed in 1732ms added theory: \Lib processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Num.thy parsed in 43ms added theory: \Num processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Pervasives.thy parsed in 21ms added theory: \Pervasives processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Ratio.thy parsed in 12ms added theory: \Ratio processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/String.thy parsed in 3ms added theory: \String processing theory file: /Users/stevenobua/myrepos/proofpeer-hollight/proofscript/Support.thy parsed in 20ms added theory: \Support
— Reply to this email directly or view it on GitHub https://github.com/proofpeer/proofpeer-proofscript/issues/33#issuecomment-57243701.
— Reply to this email directly or view it on GitHub.
The file Lib.thy fails to process in Lib.thy.