Email Gateway (Aug 18 2022 at 13:22): Email Gateway (Aug 18 2022 at 13:22):From: Tim McKenzie <tjm1983@gmail.com>
I'm trying to get Isabelle 2008's document preparation to work. I can't even
get the dry run to work, as described in section 4.2.1 of the tutorial. I've
attached the output when I run those commands, as well as the output of
pdflatex -version. I've also attached the log mentioned in the output of
isatool make. Can anyone make sense of it? It mentions that it can't find
comment.sty; where should I expect to find this?
Tim
<><
isatool-fail
HOL-MySession
signature.asc
Email Gateway (Aug 18 2022 at 13:22):From: Makarius <makarius@sketis.net>
comment.sty is often packaged as "extra" stuff, e.g. tetex-extra on some
Linux distributions.
Makarius
Email Gateway (Aug 18 2022 at 13:23):From: Tim McKenzie <tjm1983@gmail.com>
On Wednesday 15 April 2009 21:28:55 Makarius wrote:
comment.sty is often packaged as "extra" stuff, e.g. tetex-extra on some
Linux distributions.
Thanks! Your advice put me on exactly the right track, and I quickly found
texlive-latex-extra in Kubuntu. Problem solved.
Tim
<><
signature.asc
Email Gateway (Aug 19 2022 at 08:19):From: Saurabh Pradeeprao Sabnis <spsabnis@syr.edu>
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@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@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@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
"$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
Email Gateway (Aug 19 2022 at 08:19):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Saurabh,
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.
*** /root/Isabelle2011-1/lib/Tools/latex: line 75: pdflatex: command not found
This indicates that the "pdflatex" command is not available on your system. It needs to be installed to run a full session, including document generation. See the page
http://www.cl.cam.ac.uk/research/hvg/Isabelle/installation.html
for the complete list of system requirements (where "pdflatex" is implicitly part of LaTeX).
Regards,
Jasmin
Email Gateway (Aug 19 2022 at 08:19):From: Makarius <makarius@sketis.net>
Jasmin has already pointed to the missing pdflatex.
Moreover, you should not run things as "root", it is bad practice and
changes the meaning of file-system permissions in very subtle ways. For
example, Isabelle relies on the read-only mode of files in certain
situations.
Makarius
Last updated: Apr 16 2024 at 20:15 UTC