[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