Re: [isabelle] Can't generate browser_info



Dear Alessandro,

On 02/15/2013 11:06 AM, Alessandro Coglio wrote:
Following page 28 of the system manual, I tried

isabelle build -o browser_info -v -c HOL

but I get

Started at Thu Feb 14 17:59:37 PST 2013 (polyml-5.5.0_x86-darwin on
HAL9000.local)
ISABELLE_BUILD_OPTIONS=""
Just to clarify: these are the default build options that should always be added when calling "isabelle build" (you can set them in your ~/.isabelle/etc/settings). However, they are not related to what you wrote on the command line above. Sorry, that doesn't answer your actual question.


ML_PLATFORM="x86-darwin"
ML_HOME="/Applications/Isabelle2013.app/Contents/Resources/Isabelle2013/contrib/polyml-5.5.0-3/x86-darwin"
ML_SYSTEM="polyml-5.5.0"
ML_OPTIONS="-H 500"

Session Pure
Session HOL (main)
Just to make sure that everything is the same as on my machine. At this point there are many lines of output starting with

Cleaning HOL ...
Cleaning HOLCF ...
Running HOL ...
HOL: theory Code_Generator
HOL: theory HOL
HOL: theory Orderings

right? If not, it seems the "-c" flag did not work properly.

Finished at Thu Feb 14 17:59:40 PST 2013
0:00:03 elapsed time, 0:00:04 cpu time
On my machine the whole output ends with

Timing HOL (4 threads, 95.510s elapsed time, 261.987s cpu time, 22.639s GC time, factor 2.74)
Browser info at /home/griff/.isabelle/Isabelle2013/browser_info/HOL
Finished HOL (0:01:36 elapsed time, 0:04:22 cpu time, factor 2.72)
Finished at Fri Feb 15 12:14:16 JST 2013
0:01:40 elapsed time, 0:04:27 cpu time, factor 2.67

which indicates where browser_info was written. (And it was indeed written.)

Still, no real answer, but again, it seems that "-c" did not work properly.

cheers

chris






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.