Re: [isabelle] Disk usage in ~/.isabelle/contrib

On Sun, 7 Feb 2016, Gerwin Klein wrote:

This works in Linux and Mac OS X (e.g. Mountain Lion), but the latter is required to produce macos bundles. Linux can produce only linux and windows bundles, and the fonts of documentation is bad, because Gerwin and Tobias like strange fonts.

Interesting. Do you mean the Concrete Maths font? I havenʼt had any issues with it so far.

As I have pointed out some years ago, the document in question is prog-prove. On Debianistic Linux systems (e.g. Ubuntu) the result looks very ugly, with low-resolution bitmap fonts.

I guess the problem is this combination:


See also Admin/Release/CHECKLIST:

- check scalable fonts, e.g. src/Doc/Prog_Prove (NOTE: T1 encoding
  requires cm-super fonts, which are usually available on MacTeX or
  Cygwin, but not on Ubuntu/Debian);

The T1 problem was later avoided for regular LaTeX CM fonts:


This explains why most Isabelle manuals have a very long underscore, but one that can be searched for in the PDF.

Since T1 works uniformly with MacTeX (Mac OS X) and MikTeX (Windows), it is probably just due to an "improved" version of TeXLive on Debian-based systems. Someone should investigate the Debian repositories and figure out which patches needs to be removed.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.