Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Package Babel (possibly Incomplete)

Email Gateway (Aug 19 2022 at 12:41):

From: Alfio Martini <alfio.martini@acm.org>
Dear Users ,

In Isabelle 2013-1 I´m having problems with the Babel package in
the root.tex file when running my session for document
preparation. When using the "brazilian" option, I get the following
error

! Package babel Error: Unknow option `brazil'. Either you misspelled it
(babel) or the language definition file brazil.ldf was not
found

Thus I have to comment the line that calls this package. It
works well with the "english" option, though. Besides, I did not had
this problem when preparing documents with Isabelle 2013.

(Makarius), is it possible to fix this for the next release? if not,
what is the best way to upgrade the latex instalation in
cygwin? I run cigwin-setup and texlive-collection-basic seems
to be installed. So I don´t know what is going on here exactly.

Any help is greatly appreciated.

Best!

Email Gateway (Aug 19 2022 at 12:41):

From: Makarius <makarius@sketis.net>
On Tue, 26 Nov 2013, Alfio Martini wrote:

When using the "brazilian" option, I get the following error

! Package babel Error: Unknow option `brazil'. Either you misspelled it
(babel) or the language definition file brazil.ldf was not
found

Thus I have to comment the line that calls this package. It works well
with the "english" option, though. Besides, I did not had this problem
when preparing documents with Isabelle 2013.

That is just a matter how Cygwin (de)composes latex into packages, and
which of them are installed. On
http://isabelle.in.tum.de/installation.html there is a short notice as
follows:

Isabelle2013-1\Cygwin-Latex-Setup augments the Cygwin installation of
Isabelle by major parts of TeX live, as required for typical
applications of the Isabelle document preparation system.

Beyond this default setup, there are much more latex packages that can be
pulled in manually via Isabelle2013-1\Cygwin-Setup.

Altogether it can require some GBs of disk space. (On Mac OS X there is a
one-size-fits-for-all MacTeX distribution of 4.3 GB, but we don't bundle
that in the first place.)

(Makarius), is it possible to fix this for the next release?

If you point out particular Cygwin packages that are actually wrong in
Cygwin-Latex-Setup.bat, I can revisit that.

To "fix" anything, there needs to be a constructive proof that something
is actually broken.

Makarius

Email Gateway (Aug 19 2022 at 12:42):

From: Alfio Martini <alfio.martini@acm.org>
Hi Makarius,

I finally discovered the package that contains the missing files. The
problem is that TexLive in cygwin seems to adopt non
standard names for LaTeX packages. Maybe its better to leave thing in this
way, so that we install the missing data by
ourselves.

Cheers

Last updated: Apr 24 2024 at 20:16 UTC