Re: [isabelle] Generate PDF from .thy File?
In the last line below, you have commented out the filename, which is the first place to look for clues. Itâs true that the file is an exhaustive and fairly unreadable log the entire execution. But there should be a visible error message near the end. Errors from latex always begin with a ! character.
> On 15 Feb 2015, at 23:31, Bob Fang <bf283 at cam.ac.uk> wrote:
> 3. Run ``Isabelle build -D .â and I got this error:
> Running Whatever ...
> Whatever FAILED
> (see also â)
This archive was generated by a fusion of
Pipermail (Mailman edition) and