[isabelle-dev] html output of theories

Makarius makarius at sketis.net
Wed Apr 16 14:47:58 CEST 2014


On Mon, 14 Apr 2014, Gottfried Barrow wrote:

> (RULE1) Do not do something that may be beneficial in the short term but 
> ties you into something for the long term you don't want to be tied 
> into.
>
> That "something" is Cygwin texlive. Cygwin like you're using, as a fast 
> form of Unix for Windows, is an amazing thing, but I don't see texlive 
> ever being supported like the native Windows LaTeX distributions, such 
> as MiKTeX. I did run Cygwin-Latex-Setup.bat, and it did an effortless 
> setup. However, there's the magic retrieval of packages I get with 
> MiKTeX. Also, I use portable MiKTeX because I got tired of continually 
> doing setup for a LaTeX distribution.

I started recently to wonder about the question of latex installations on 
Windows.  Is MikTeX *the* thing to look at?  There also seems to be a 
Windows version of TeXlive, but maybe that is just an odd minority thing?

I suspect that Isabelle document preparation could use an existing LaTeX 
for Windows with minimal changes to the setup, bypassing Cygwin.  Then 
Isabelle users on Windows would be in the same boat as Mac OS X or Linux, 
by relying implicitly on what happens to be there.  That is usually the 
habitual LaTex installation, but in rare situations something that does 
not work for unclear reasons.


 	Makarius



More information about the isabelle-dev mailing list