Email Gateway (Aug 19 2022 at 13:23): Email Gateway (Aug 19 2022 at 13:23):From: James Lingard <james@lingard.com>
I'm new to Isabelle, and am struggling to get the document preparation
system to work for the first time. Here's what I tried:
$ isabelle mkroot -d test
...
$ isabelle build -D test
...
This successfully creates a dummy test/output/document.pdf file. Now I
create the simplest possible theory file, and try to incorporate that:
$ cat > test/mytheory.thy
theory mytheory imports Main
begin
end
$ vi test/ROOT # to add mytheory
$ cat test/ROOT
session "test" = "HOL" +
options [document = pdf, document_output = "output"]
theories [document = false]
(* Foo Bar *)
theories
mytheory (* Baz *)
files "document/root.tex"
Now the build fails with a bizarre LaTeX error:
$ isabelle build -D test
Running test ...
test FAILED
(see also
/Users/jchl/.isabelle/Isabelle2013-2/heaps/polyml-5.5.1_x86-darwin/log/test)
*** [Loading MPS to PDF converter (version 2006.09.02).]
*** )
(/usr/local/texlive/2013basic/texmf-dist/tex/latex/hyperref/nameref.sty
*** (/usr/local/texlive/2013basic/texmf-dist/tex/generic/oberdiek/
gettitlestring.st
*** y)) (./root.out) (./root.out) (./root.toc) (./session.tex
(./mytheory.tex
*** Including 'isadelimtheory' comment.)
*** Runaway argument?
*** ! File ended while scanning use of \next.
*** <inserted text>
*** \par
*** l.1 \input{mytheory.tex}
*** ))
*** ! Emergency stop.
*** <*> \nonstopmode\input{root.tex}
*** ! ==> Fatal error occurred, no output PDF file produced!
*** Transcript written on root.log.
*** Document preparation failure in directory 'output/document'
*** Failed to build document "/Users/jchl/test/output/document.pdf"
Unfinished session(s): test
0:00:10 elapsed time, 0:00:16 cpu time, factor 1.60
Can anyone help me understand what (if anything) I'm doing wrong, and how I
can fix it?
Version info:
Thanks,
James.
Email Gateway (Aug 19 2022 at 13:23):From: Makarius <makarius@sketis.net>
That is a latex error, so it just depends on the actual sources that are
given to it. It is all in the directory "output/document" mentioned
above. You can cd there and just run pdflatex directly, and look closely
again what is there in the files. There is some chance that some odd
control characters somehow sneaked in (maybe via "cat"), or something
completely different and unexpected.
If you still don't see it, just send me the actual output/document/
content.
Some side-remarks:
* Isabelle session names and theory names consist of capitalized words
(separated by underscores), e.g. Foo, Bar, Baz, My_Theory. Almost
everything inside a theory uses lowercase names (including types, but
excluding datatype constructors).
* Isabelle/jEdit takes some time to start-up, but once it is running it
is able to edit text files conveniently, including ROOT.
I have recently learned about the server mode of jEdit, which is off by
default. If enabled it is easy to delegate edit tasks from the
command-line to an already running jEdit application. (That might be
worth a different mailing list thread.)
Makarius
Email Gateway (Aug 19 2022 at 13:23):From: Makarius <makarius@sketis.net>
Just before the test, I had updated to recent MacTeX-2013 and its
/usr/local/texlive/2013/texmf-dist/tex/latex/comment/comment.sty is still
at version 3.6.
Looking briefly at
http://www.ctan.org/tex-archive/macros/latex2e/contrib/comment has the
same 3.6 number in the blurb, but there is a brand-new version 3.7:
comment.sty 9666 2014-01-23 07:36:21
Its inlined changelog says:
Changes in 3.7
% - only LaTeX support from now on
% - code cleanup, and improvements on \specialcomment
% - cleanup of the docs.
This means it cannot be used with isabelle.sty, because of that:
%plain TeX version of comment package -- much faster!
\let\isafmtname\fmtname\def\fmtname{plain}
\usepackage{comment}
\let\fmtname\isafmtname
If comment.sty 3.7 is actually better in latex mode now, it might be worth
revisiting. But by default this is just a normal instance of "latex
package version hell".
Makarius
Email Gateway (Aug 19 2022 at 13:23):From: Makarius <makarius@sketis.net>
So from where did you get that version? TeXlive is not there yet,
luckily.
I use myself CTAN only as occasional reference, but have no idea how it is
actually maintained. There is also no immediately visible changeset
history, with names of authors etc.
Maybe it is just an accident, with some experiment that someone made at
some point, to the anoyance of plain TeX users.
Makarius
Email Gateway (Aug 19 2022 at 13:24):From: Makarius <makarius@sketis.net>
Oh dear. I didn't know yet, that TeXlive has its own package manager to
get latest problems quicker to users.
I need to think about evasive maneuvers, for the next Isabelle release.
This continous "fixing" of things, destroys everything eventually.
Makarius
Email Gateway (Aug 19 2022 at 13:24):From: James Lingard <james@lingard.com>
Hi Makarius,
Thanks for the response. I dived into the LaTeX sources, and it turns out
that the problem was that I was using the "wrong" version of comment.sty.
I was using the most recent version, version 3.7 (which dates from 2009).
It seems that Isabelle requires version 3.6.
Thanks,
James.
Email Gateway (Aug 19 2022 at 13:24):From: James Lingard <james@lingard.com>
On 29 January 2014 15:10, Makarius <makarius@sketis.net> wrote:
On Wed, 29 Jan 2014, James Lingard wrote:
I dived into the LaTeX sources, and it turns out that the problem was
that I was using the "wrong" version of comment.sty. I was using the most
recent version, version 3.7 (which dates from 2009). It seems that Isabelle
requires version 3.6.
Just before the test, I had updated to recent MacTeX-2013 and its
/usr/local/texlive/2013/texmf-dist/tex/latex/comment/comment.sty is still
at version 3.6.Looking briefly at http://www.ctan.org/tex-archive/macros/latex2e/
contrib/comment has the same 3.6 number in the blurb, but there is a
brand-new version 3.7:comment.sty 9666 2014-01-23 07:36:21
That's weird. The copyright at the top of the file says July 2009. If it
really is brand new then that explains why I might have been the first
person to run into this.
Thanks,
James.
Its inlined changelog says:
Changes in 3.7
% - only LaTeX support from now on
% - code cleanup, and improvements on \specialcomment
% - cleanup of the docs.This means it cannot be used with isabelle.sty, because of that:
%plain TeX version of comment package -- much faster!
\let\isafmtname\fmtname\def\fmtname{plain}
\usepackage{comment}
\let\fmtname\isafmtnameIf comment.sty 3.7 is actually better in latex mode now, it might be worth
revisiting. But by default this is just a normal instance of "latex
package version hell".Makarius
Email Gateway (Aug 19 2022 at 13:24):From: James Lingard <james@lingard.com>
On 29 January 2014 19:32, Makarius <makarius@sketis.net> wrote:
On Wed, 29 Jan 2014, James Lingard wrote:
comment.sty 9666 2014-01-23 07:36:21
That's weird. The copyright at the top of the file says July 2009. If
it
really is brand new then that explains why I might have been the first
person to run into this.
So from where did you get that version? TeXlive is not there yet, luckily.
I installed it on Tuesday with "tlmgr install comment".
James.
I use myself CTAN only as occasional reference, but have no idea how it is
actually maintained. There is also no immediately visible changeset
history, with names of authors etc.Maybe it is just an accident, with some experiment that someone made at
some point, to the anoyance of plain TeX users.Makarius
Email Gateway (Aug 19 2022 at 13:25):From: Makarius <makarius@sketis.net>
I've looked again more closely at CTAN: the situation of
http://www.ctan.org/tex-archive/macros/latex2e/contrib/comment is a bit
odd, because comment.sty has been copied over with that 3.7 version from
2009, while everything else is still saying 3.6, including the
documentation (which claims that the package works with Plain TeX).
I've also tried again if it is feasible to run in regular LaTeX mode, but
then it is very slow, as already noticed in 2005, when I made this setup
for isabelle.sty.
So the present conclusion of this thread: Anybody who happens to be on a
latest-testing-unstable branch of some TeX installation can put a copy of
the included comment.sty 3.6 into $ISABELLE_HOME/lib/texinputs/. The
Isabelle document preparation system will copy it from there into the
document output directory, so that version should take precedence.
The next Isabelle release will probably have that comment.sty 3.6 as well,
but that is still several months ahead.
Makarius
comment.sty
Email Gateway (Aug 19 2022 at 15:31):From: bnord <bnord01@gmail.com>
Just wanted to pop this up again as the issue persists with 2014-RC4 and
comment.sty version 3.7 is in the stable branch of tex live.
Best
Benedikt
Email Gateway (Aug 19 2022 at 15:33):From: Makarius <makarius@sketis.net>
On Thu, 21 Aug 2014, bnord wrote:
Just wanted to pop this up again as the issue persists with 2014-RC4 and
comment.sty version 3.7 is in the stable branch of tex live.
What exactly do you mean by "the issue persists"?
The approach from 29-Jan-2014 still works today: using comment.sty 3.6
before the desastrous "fix". A copy of it was already included in all
Isabelle2014 release candidates, so it should work by default, if
documents are built the standard way. The "system" manual has an example
for that:
isabelle mkroot -d Test && isabelle build -D Test
You can then look in Test/output/document/root.log to see that a local
copy of comment.sty is used. If not, there is something utterly wrong.
Makarius
Am 31.01.14 19:44, schrieb Makarius:
On Wed, 29 Jan 2014, Makarius wrote:
On Wed, 29 Jan 2014, James Lingard wrote:
comment.sty 9666 2014-01-23 07:36:21
That's weird. The copyright at the top of the file says July 2009.
If it
really is brand new then that explains why I might have been the
first
person to run into this.So from where did you get that version? TeXlive is not there yet,
luckily.I use myself CTAN only as occasional reference, but have no idea how it
is actually maintained. There is also no immediately visible changeset
history, with names of authors etc.Maybe it is just an accident, with some experiment that someone made at
some point, to the anoyance of plain TeX users.I've looked again more closely at CTAN: the situation of
http://www.ctan.org/tex-archive/macros/latex2e/contrib/comment is a bit
odd, because comment.sty has been copied over with that 3.7 version from
2009, while everything else is still saying 3.6, including the
documentation (which claims that the package works with Plain TeX).I've also tried again if it is feasible to run in regular LaTeX mode, but
then it is very slow, as already noticed in 2005, when I made this setup
for isabelle.sty.So the present conclusion of this thread: Anybody who happens to be on a
latest-testing-unstable branch of some TeX installation can put a copy of
the included comment.sty 3.6 into $ISABELLE_HOME/lib/texinputs/. The
Isabelle document preparation system will copy it from there into the
document output directory, so that version should take precedence.The next Isabelle release will probably have that comment.sty 3.6 as well,
but that is still several months ahead.Makarius
Email Gateway (Aug 19 2022 at 15:33):From: bnord <bnord01@gmail.com>
Sorry, my bad. There was some interference in my test case.
Last updated: Apr 19 2024 at 04:17 UTC