Re: [isabelle] Easier quick PDF generation possible?



I could even imagine a button in Isabelle/JEdit to generate the
document and place it in the Document tab on the right.

And, isabelle build seems to be slow, does it use the information from
the continuous proof checking? I guess not. If it were part of
Isabelle/JEdit, it would be much different.

On 23 October 2014 13:44, Joachim Breitner <breitner at kit.edu> wrote:
> Hi,
>
> I just create a small theory to do a quick experiment, and I wanted to
> share it with someone. Isabelle can create pretty PDF output, so I
> wanted to share it as such, but this turns out to be a task that is
> unnecessary complicated.
>
> Here is my log:
>
> 1. run "isabelle mkroot"
> 2. notice that I ran it wrong, "rm ROOT"
> 3. run "isabelle mkroot -d"
> 4. add my theory to ROOT, removed the theories [document = false]
>    section, because empty sections are not allowed
> 5. run "isabelle build -D"
> 6. noticed that a few other theories were pulled in that I did not want
> 7. tried to add their theory names to the [document = false] section,
>    for which I first had to look up the syntax in another ROOT file
> 8. noticed that this did not work. Put in the theory path (i.e.
>    "~~/src/HOL/Library/Extended_Real") in there
> 9. adjusted document/root.txt to have a proper title and not disclose my
>    local username
>
> Here is what I would have liked to do:
>
> 1. run "isabelle thy2pdf Foo.thy"
>
>
> So if anyone agrees that this would be useful, and is able to implement
> this minor feature suggestion, I’d appreciate that!
>
> Thanks,
> Joachim
>
>
> --
> Dipl.-Math. Dipl.-Inform. Joachim Breitner
> Wissenschaftlicher Mitarbeiter
> http://pp.ipd.kit.edu/~breitner




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