Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle document fails with non-descriptive e...

view this post on Zulip Email Gateway (Aug 03 2020 at 10:47):

From: "Max W. Haslbeck" <max.haslbeck@gmx.de>
Hi everyone,

We ran into the following problem last week when we had a new submission to the AFP.

Consider this minimal Isabelle session (see also the attached archive):

The ROOT file has the following content:

session Minimal = HOL +
  theories
    Submission
  document_files
    "root.tex"
    "root.bib"

The root.tex file is a minimal Isabelle LaTeX file with NO \bibliography command.

The command isabelle build -d . -o document=pdf Minimal has the following output:

Running Minimal ...
Minimal FAILED
(see also /Users/mhaslbeck/.isabelle/Isabelle2020/heaps/polyml-5.8.1_x86_64-darwin/log/Minimal)
Loading theory "Minimal.Submission"
### theory "Minimal.Submission"
### 0.014s elapsed time, 0.027s cpu time, 0.000s GC time
isabelle document -d /Users/mhaslbeck/.isabelle/Isabelle2020/browser_info/Unsorted/Minimal/document -o pdf -n document
*** Failed to build document in "/Users/mhaslbeck/.isabelle/Isabelle2020/browser_info/Unsorted/Minimal/document"
Unfinished session(s): Minimal
0:00:05 elapsed time

The "*** Failed to build …" line is the only error message I was able to find and nothing more. isabelle document seems to have a problem with the reference to the root.bib file in the ROOT file that then isn’t actually used in root.tex.

If I remove the reference to "root.bib" from the ROOT file, the build process succeeds. Or I can add

\cite{LNCS2283}
\bibliographystyle{abbrv}
\bibliography{root}

to root.tex for a successful build.

So, I just wanted to report that. I think, a more descriptive error message would be helpful here.

Gruß
Max
minimal_isabelle_document_session.zip

view this post on Zulip Email Gateway (Aug 03 2020 at 16:26):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Max,

The root.tex file is a minimal Isabelle LaTeX file with NO \bibliography command.

The command isabelle build -d . -o document=pdf Minimal has the following output:
```
Running Minimal ...
Minimal FAILED
(see also /Users/mhaslbeck/.isabelle/Isabelle2020/heaps/polyml-5.8.1_x86_64-darwin/log/Minimal)
Loading theory "Minimal.Submission"

theory "Minimal.Submission"

0.014s elapsed time, 0.027s cpu time, 0.000s GC time

isabelle document -d /Users/mhaslbeck/.isabelle/Isabelle2020/browser_info/Unsorted/Minimal/document -o pdf -n document
*** Failed to build document in "/Users/mhaslbeck/.isabelle/Isabelle2020/browser_info/Unsorted/Minimal/document"
Unfinished session(s): Minimal
0:00:05 elapsed time

as far as I know this terse message is due to bibtex returning a non-0
exit value without further error messages in absence of bib entries,
making the &&-chain

bash(
List(
latex_bash("sty"),
latex_bash(document_format),
"{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }", (***)
"{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }",
latex_bash(document_format),
latex_bash(document_format)).mkString(" && "))

in present.scala break at (***), where bibtex is called by «isabelle
latex -o bbl«

Maybe an explicit error message issued by isabelle latex in that case
would be appropriate. But that would need further investigation.

Cheers,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 31 2020 at 14:59):

From: Makarius <makarius@sketis.net>
I have investigated this: the bibtex tool is very old-fashioned, and does not
know about Unix conventions for stdout vs. stderr.

So I have inserted a little perl magic (for the Isabelle2021 release,
presumably in Feb-2021): https://isabelle-dev.sketis.net/rISABELLE4710dd5093a3

The result is like this:

Running Minimal ...
Minimal FAILED
(see also /home/makarius/.isabelle/heaps/polyml-5.8.2_x86_64_32-linux/log/Minimal)
Loading theory "Minimal.Submission"

theory "Minimal.Submission"

0.026s elapsed time, 0.051s cpu time, 0.000s GC time

isabelle document -d output/document -o pdf -n document
*** bibtex found no \citation commands---while reading file root.aux
*** bibtex found no \bibdata command---while reading file root.aux
*** bibtex found no \bibstyle command---while reading file root.aux
*** Failed to build document in "/home/makarius/tmp/Minimal/output/document"
Unfinished session(s): Minimal

Makarius

Last updated: Jan 04 2025 at 20:18 UTC