[isabelle] Document preparation




Hello all,


I am currently in the learning stage of the Isabelle/HOL .. I can't even work out the dry run . I am getting error. I checked all files and folder. They are in the right position and have the right permissions.

commands are performed according to the tutorial.(4.2.1 Isabelle Sessions)

Please help me out .. there must be some fault and I can not get hold of it..


root at saurabh-DX4860:~/Isabelle2011-1/bin# ./isabelle mkdir HOL MySession
Preparing session "MySession" ...
creating ./IsaMakefile
creating ./MySession/ROOT.ML
creating ./MySession/document
creating ./MySession/document/root.tex

Notes:

  * 'isabelle make' processes the session (including document preparation)

  * ./IsaMakefile contains compilation options and file dependencies

  * ./MySession/document/root.tex contains the LaTeX master document setup

  * ./MySession/ROOT.ML needs to contain ML code to load all theories


Hello all,


I am currently in the learning stage of the Isabelle/HOL .. I can't even work out the dry run . I am getting error. I checked all files and folder. They are in the right position and have the right permissions.

commands are performed according to the tutorial.(4.2.1 Isabelle Sessions)

Please help me out .. there must be some fault and I can not get hold of it..


root at saurabh-DX4860:~/Isabelle2011-1/bin# ./isabelle mkdir HOL MySession
Preparing session "MySession" ...
creating ./IsaMakefile
creating ./MySession/ROOT.ML
creating ./MySession/document
creating ./MySession/document/root.tex

Notes:

  * 'isabelle make' processes the session (including document preparation)

  * ./IsaMakefile contains compilation options and file dependencies

  * ./MySession/document/root.tex contains the LaTeX master document setup

  * ./MySession/ROOT.ML needs to contain ML code to load all theories


root at saurabh-DX4860:~/Isabelle2011-1/bin# ./isabelle make
Running HOL-MySession ...
Browser info at /root/.isabelle/Isabelle2011-1/browser_info/HOL/MySession
HOL-MySession FAILED
(see also /root/.isabelle/Isabelle2011-1/heaps/polyml-5.4.0_x86_64-linux/log/HOL-MySession)

> val it = (): unit
val commit = fn: unit -> bool
### Browser info: cannot access session index of "/root/.isabelle/Isabelle2011-1/browser_info/HOL"
"$ISABELLE_TOOL" document -c -o 'pdf' -n 'outline' -t '/proof,/ML' '/root/.isabelle/Isabelle2011-1/browser_info/HOL/MySession/outline' 2>&1
"$ISABELLE_TOOL" document -c -o 'pdf' -n 'document' -t '' '/root/.isabelle/Isabelle2011-1/browser_info/HOL/MySession/document' 2>&1
*** /root/Isabelle2011-1/lib/Tools/latex: line 75: pdflatex: command not found
*** Document preparation failure in directory '/root/.isabelle/Isabelle2011-1/browser_info/HOL/MySession/document'
***
*** Failed to build document "/root/.isabelle/Isabelle2011-1/browser_info/HOL/MySession/document.pdf"

make: *** [/root/.isabelle/Isabelle2011-1/heaps/polyml-5.4.0_x86_64-linux/log/HOL-MySession.gz] Error 1


Thanks and regards

Saurabh Sabnis





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