Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Document Preparation System - Windows

Email Gateway (Aug 22 2022 at 11:33):

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

This is the first time I am using the document preparation system in
Isabelle 2015 (Windows). It works,
but there are plenty of warning/error messages concerning Perl. Image is
attached.

Am I missing something?

Best!
isabelle_perl.PNG

Email Gateway (Aug 22 2022 at 11:33):

From: Makarius <makarius@sketis.net>
I see merely warnings here: the document should have been produced
properly.

The reason why perl complains: the environment variable LANG is set to
"PT", but that does not conform to any of the POSIX locales. E.g. try
this on the Cygwin command-line:

$ locale -a | grep -i pt
pt_BR
pt_BR.utf8
pt_PT
pt_PT.utf8
pt_PT@euro

I guess that you want pt_BR.utf8. This can be enforced by editing
/etc/profile.d/lang.sh for example.

If you are unfamiliar with the Cygwin command-line and its POSIX tools
(like vi) you can edit the file with Isabelle/jEdit under the Windows
name %ISABELLE_HOME%\contrib\cygwin\etc\profile.d\lang.sh

The end of the last line looks like this:

export LANG=$(/usr/bin/locale -uU)

If you try "locale -uU" manually on the command line, what does it show?

You can also replace the expression $(/usr/bin/locale -uU) by "pt_BR.utf8"
or even just "C".

Another source of problems might be an already existing LANG variable with
a bad value.

Makarius

Email Gateway (Aug 22 2022 at 11:37):

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

Thanks for your remarks. Yes, it works, but I would like to get rid of
those warnings (if possible).
I did not have this issue with Isabelle 2014.

I installed a fresh copy of Isabelle 2015. But the same problem occurs;

If you try "locale -uU" manually on the command line, what does it show?

Alfio@isabelle ~/Desktop/Isabelle2015
$ locale -uU
en_GB.UTF-8

You can also replace the expression $(/usr/bin/locale -uU) by "pt_BR.utf8"
or even just "C".

I tried both options but it did not work.

Thanks anyway! In the worst case scenario, I will download Isabelle2014 for
typesetting
documents.

Best!

On Fri, Oct 23, 2015 at 6:01 PM, Makarius <makarius@sketis.net> wrote:

On Wed, 21 Oct 2015, Alfio Martini wrote:

This is the first time I am using the document preparation system in

Isabelle 2015 (Windows). It works, but there are plenty of warning/error
messages concerning Perl. Image is attached.

I see merely warnings here: the document should have been produced
properly.

The reason why perl complains: the environment variable LANG is set to
"PT", but that does not conform to any of the POSIX locales. E.g. try this
on the Cygwin command-line:

$ locale -a | grep -i pt
pt_BR
pt_BR.utf8
pt_PT
pt_PT.utf8
pt_PT@euro

I guess that you want pt_BR.utf8. This can be enforced by editing
/etc/profile.d/lang.sh for example.

If you are unfamiliar with the Cygwin command-line and its POSIX tools
(like vi) you can edit the file with Isabelle/jEdit under the Windows name
%ISABELLE_HOME%\contrib\cygwin\etc\profile.d\lang.sh

The end of the last line looks like this:

export LANG=$(/usr/bin/locale -uU)

If you try "locale -uU" manually on the command line, what does it show?

You can also replace the expression $(/usr/bin/locale -uU) by "pt_BR.utf8"
or even just "C".

Another source of problems might be an already existing LANG variable with
a bad value.

Makarius

Email Gateway (Aug 22 2022 at 11:37):

From: Makarius <makarius@sketis.net>
On Tue, 27 Oct 2015, Alfio Martini wrote:

If you try "locale -uU" manually on the command line, what does it show?

Alfio@isabelle ~/Desktop/Isabelle2015
$ locale -uU
en_GB.UTF-8

This looks fine so far.

You can also replace the expression $(/usr/bin/locale -uU) by "pt_BR.utf8"
or even just "C".

I tried both options but it did not work.

My guess from a distance is that the Windows environment provides a value
for LANG=PT, which is then not challanged by the Cygwin startup scripts.

If you just edit Isabelle2015\Cygwin-Terminal.bat you can set a different
value there, e.g.

set LANG=en_GB.UTF-8

Makarius

Email Gateway (Aug 22 2022 at 11:38):

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

If you just edit Isabelle2015\Cygwin-Terminal.bat you can set a different

Last updated: Apr 25 2024 at 04:18 UTC